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