Arithmetic normalization now handles relations and Sym.simp (
33bb0aa)
Sym.Arith.normalize? now normalizes =, ≤, and < over commutative rings and semirings, moving terms to one side and simplifying to polynomial normal form. That lets the arith simproc close goals when both sides reduce to the same polynomial, and extends Sym.simp with an opt-in arithmetic pre-simproc.
Runtime RC overflow handling is hardened (
2b21d8b, 
8546083)
The runtime now distinguishes ordinary sticky counts from counts that overflowed out of the single-threaded range, and treats both as unshared where appropriate. This closes a potential undefined-behavior hole in sharing/deletion cascades by ensuring children of overflowed objects are also marked thread-shared or preserved correctly.
Discrimination trees gain a single-child chain form (
fbfa241)
DiscrTree now represents no-value single-child nodes with a dedicated .chain branch instead of a full node. This is a memory-optimized refactor that also touches insertion, matching, and pretty-printing, so it should reduce overhead in common trie-heavy uses like simplification.
Deprecated tactic warnings are deduplicated per call (
3baf820)
Deprecated tactics now warn at most once per invocation, even if the tactic expands into multiple deprecated uses internally. This cuts noisy repeated warnings for expansions like mintro a b c while preserving the deprecation signal.
