Coq 8.5 beta 1 is out!
Submitted by coq-www on 21 Jan 2015 15:00 GMT
The first beta release of Coq 8.5 is available for
testing. The 8.5 version brings several major features to Coq:
- 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);
- a new tactic engine allowing dependent subgoals, 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).