Coq 8.10.2

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.


FWIW, it’s also coming on opam:,


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!

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

Complete changelog, from 8.4 to 8.10 can be found here: