Skip to content

@vbgl vbgl released this Oct 8, 2019 · 1770 commits to master since this release

Coq 8.10.0 contains:

  • 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.

Assets 6
You can’t perform that action at this time.