Coq 8.5pl3

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

5.2 MB
94 MB
92 MB
CoqIDE_8.5pl3.dmg (bundled with CoqIDE, compiled using OCaml 4.02.3 and Camlp5 6.14) 125 MB
0.2 MB
1.6 MB