The final release of Coq 8.5 is available! 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 can be found in the CHANGES file.