Release 2025.10

What's Changed

• add Reflection theory by @oskgo in #794
• List: new lemmas: nth0, nth1, map1, head_drop by @namasikanam in #796
• [tactic] Single sided match should work for arbitrary pre-conditions by @Cameron-Low in #795
• [tactic] Actually improve one-sided match robustness by @Cameron-Low in #800
• Rework import mechanism by @strub in #683
• extend results on ceil 'for free' by @fdupress in #781
• depext -> confirm level = unsafe-yes by @strub in #798
• remove alt-ergo from EasyCrypt TCB by @fdupress in #724
• EcRegexp: PCRE -> PCRE2 by @strub in #797
• Introduce a system-wide, parts-oriented configuration file by @strub in #801
• OCaml 5 memory blowup workaround by @strub in #802
• Rework stdlib clones. by @strub in #694
• Give a proof to witness_support by @fdupress in #803
• add mu_has_le in rewrite Pr by @bgregoir in #804
• List: new lemmas: subseq_catR, subseq_catL, subseq_consI, subseq_take, subseq_drop, subseq_drop_congr by @namasikanam in #807
• Exit --help with non-error status by @MM45 in #808
• New result: List.sorted_range by @strub in #815
• More results on List.zip by @strub in #813
• More results on BitEncoding.int2bs by @strub in #814

New Contributors

• @namasikanam made their first contribution in #796

Full Changelog: r2025.08...r2025.10