Coq 8.5pl3

The current version: Coq 8.5pl3

This version features:

  • asynchronous edition of documents under CoqIDE to keep working on a proof while Coq checks the other proofs in the background (by Enrico Tassi);
  • universe polymorphism making it possible to reuse the same definitions at various universe levels (by Matthieu Sozeau);
  • primitive projections improving space and time efficiency of records, and adding eta-conversion for records (by Matthieu Sozeau);
  • new extensions of the proof engine featuring dependent subgoals management, fully backtracking tactics, as well as tactics which can consider multiple goals together (by Arnaud Spiwack);
  • a new reduction procedure called native_compute to evaluate terms using the OCaml native compiler, for proofs with large computational steps (by Maxime Dénès).

The main other changes are:

  • a new fast compilation chain that skips checking of proofs (producing .vio files);
  • a new construct ltac:(..) to call tactics from term definitions;
  • a more restrictive guard condition to recover compatibility with axioms like propositional extensionality and (some consequences of) univalence;
  • a new option -type-in-type to collapse the universe hierarchy (makes the logic inconsistent but useful for exploration);
  • a better-behaved alternative to simpl, called cbn;
  • various improvements to the tactic language, like a new introduction pattern [= x1 ... xn] which applies injection on the fly (inspired by SSReflect);
  • a new construct uconstr:c and type_term c to build untyped terms in Ltac;
  • significant improvements on efficiency in general.

For a log of changes, see the file CHANGES.

Coq 8.5 is not entirely upward compatible with 8.4

Sources
5.2 MB
Binaries
windows
Windows
94 MB
windows
Windows
92 MB
macos
MacOS
CoqIDE_8.5pl3.dmg (bundled with CoqIDE, compiled using OCaml 4.02.3 and Camlp5 6.14) 125 MB
Documentation
0.2 MB
1.6 MB