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
|coq-installer-8.5pl3-win32.exe (32 bits, bundled with CoqIDE, compiled using CoqSDK)||94 MB|
|coq-installer-8.5pl3-win64.exe (64 bits, bundled with CoqIDE, compiled using CoqSDK 64 bits)||92 MB|
|CoqIDE_8.5pl3.dmg (bundled with CoqIDE, compiled using OCaml 4.02.3 and Camlp5 6.14)||125 MB|
|Reference-Manual.pdf (also online)||1.6 MB|
|Standard Library online documentation|