- Update to version 8.11.0.
  * Ltac2, a new tactic language for writing more robust larger
    scale tactics, with built-in support for datatypes and the
    multi-goal tactic monad.
  * Primitive floats are integrated in terms and follow the binary64
    format of the IEEE 754 standard, as specified in the
    Coq.Float.Floats library.
  * Many other cleanups and improvements have been performed and
    are further described in the changelog.
  * Special note on compatibility: Fixed bugs of Export and Import
    that can have a significant impact on user developments.
- Drop unneeded empty *.vos files.
- Update to version 8.10.2.
  * 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.
- Update to version 8.10.0.
  * 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.
- Update to version 8.10.1.
  * Fix proof of False when using SProp
  * Fix an anomaly when unsolved evar in Add Ring
  * Fix Ltac regression in binding free names in uconstr
  * Fix handling of unicode input before space
  * Fix custom extraction of inductives to JSON
- Update version requirements.

• Files Changed
• Browse Source