Version 8.5pl2 of Coq is available. It fixes several bugs of version 8.5pl1, including one critical bug. More information can be found in the CHANGES file.

Version 8.5pl1 of Coq is available. It fixes several bugs of version 8.5, including one critical bug. It also brings various performance improvements. More information can be found in the CHANGES file.

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.

Version 8.4pl6 of Coq fixes several bugs of version 8.4pl5. More information to be found in the CHANGES file.

Version 8.4pl5 of Coq fixes several bugs of version 8.4pl4 including the compatibility with OCaml 4.02. More information to be found in the CHANGES file.