Coq 8.10.0 is out

The 8.10.0 release of Coq is available.

Main changes:

  • some quality-of-life bug fixes;
  • a critical bug fix related to template polymorphism;
  • native 63-bit machine integers;
  • a new sort of definitionally proof-irrelevant propositions: SProp;
  • private universes for opaque polymorphic constants;
  • string notations and numeral notations;
  • a new simplex-based proof engine for the tactics lia, nia, lra and nra;
  • new introduction patterns for SSReflect;
  • a tactic to rewrite under binders: under;
  • easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.

All details can be found in the user manual.

Feedback and bug reports are extremely welcome.