Coq 8.10.2

Announcements
1

The 8.10.2 release of Coq is available.

Main changes:

  • Fixed a critical bug of template polymorphism and nonlinear universes
  • Fixed a few anomalies
  • Fixed an 8.10 regression related to the printing of coercions associated to notations
  • Fixed uneven dimensions of CoqIDE panels when window has been resized
  • Fixed queries in CoqIDE

All details can be found in the user manual.

Feedback and bug reports are extremely welcome.

4 Likes
2

FWIW, it’s also coming on opam: https://github.com/ocaml/opam-repository/pull/15416, https://github.com/ocaml/opam-repository/pull/15417.

2 Likes
3

Excuse me, I’m learning to use coq recently. I have a project based on 8.4, but now I want to port to 8.10.2. I know that the changes between these two versions are large, but can you give me some suggestions about Migration issue? thank you very much!

4

Your best bet is doing the migration one-version-at-a-time; depending on the ltac hackery you are using it should be easy or pretty hard; expect the most trouble in the jump from 8.4 to 8.5 tho, the rest should be doable as long as you read the Changelog; if you find some problem you don’t understand you can ask the devs here or in Gitter.

1 Like
5

Complete changelog, from 8.4 to 8.10 can be found here: https://coq.inria.fr/refman/changes.html