Mathcomp 2.6.0 released

Announcements
1

We are proud to announce the immediate availability of the Mathematical Components library version 2.6.0
The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Rocq 9.0 to 9.3+rc1

The main changes are:

  • removed Global Set SsrOldRewriteGoalsOrder in ssreflect.v, for a smooth transition, we recommend adding
    Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
    in each of your files after requiring ssreflect.v (even indirectly), which will enable porting to the new rewrite subgoals order on a file per file basis
  • new files ring_tactic.v, field_tactic.v andarithmetic_tactic.v in the mathcomp-algebra package, offering decision procedures ring, field and lra respectively (formerly
    available in the mathcomp-algebra-tactics package)
  • new file tensor.v, this remains experimental and may change without deprecation warning in the next release
  • packages fingroup and character have been renamed tofinite-group and group-representation respectively
  • many generalization, file splitting and cleanup, these should ideally remain transparent to users or at worst easy to adapt to, following the deprecation messages

See the CHANGELOG.md file for more details.

The contributors to this version are: Reynald Affeldt, Valentin Blot, Alessandro Bruni, Cyril Cohen, Florent Hivert, Marie Kerjean, Vincent Laporte, Pierre Roux, Takafumi Saikawa, Kazuhiko Sakaguchi, Joshua Smart, Laurent Théry, Holger Thies, Quentin Vermande, Li Zhou

We also wish to thank all the reviewers of the various contributions.

See Release The Mathematical Components Library 2.6.0 · math-comp/math-comp · GitHub to download.

Packages for opam, nix, and docker images are available.

Best regards,

The Mathematical Components team