Release 2025.03

What's Changed

Tactics

• Extend clear tactic to allow clearing all unused items in the context recursively by @oskgo in #713
• Improvements to module tweaks by @Cameron-Low in #728
• Reworked outline tactic by @Cameron-Low in #727
• New vernacular command: theory aliases by @strub in #685

Standard library

• Disambiguate precedence in negbLR and negbRL and add new lemmas for left and right distributivity by @oskgo in #737
• Multisets by @oskgo in #722
• reduce number of axioms in Logic by @oskgo in #751
• Add list lemmas and shorten some other proofs using them by @MM45 in #721
• stdlib: in Field, do not erase the unit predicate by @strub in #757

Bug fixes

• Pretty printer: print terminator after module types by @ruipedro16 in #723
• Fix return of properties with provided bit in KEM/PKE libraries by @MM45 in #738
• Fix HC collisions. by @strub in #739
• Minor fixes for sim by @Cameron-Low in #743
• Hi-level error message when subst fails by @strub in #734
• Hi-level error message in clone (axiom <-) by @strub in #748
• fix tactic ehoare-if by @bgregoir in #754

Internals

• [internal] introduce general code position ranges for selecting code blocks. by @Cameron-Low in #709
• remove duplicated code from EcAst by @strub in #731

Chores

• CI: update image from ubuntu-20.04 to ubuntu-24.04 by @strub in #736

New Contributors

• @ruipedro16 made their first contribution in #723

Full Changelog: r2025.02...r2025.03