Home

Coq 8.5 beta 2 is out!

Submitted by Matthieu Sozeau on 22 Apr 2015 19:00 GMT
The second 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).
More information about the changes from 8.4 to 8.5 and since the first beta release can be found in the CHANGES file. Feedback and bug reports are extremely welcome. Enjoy!