Coq 8.5
The current version: Coq 8.5
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 etaconversion 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 typeintype to collapse the universe hierarchy (makes the logic inconsistent but useful for exploration);
 a betterbehaved 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 full log of changes, see the file CHANGES.
Coq 8.5 is not entirely upward compatible with 8.4
Sources  
coq8.5.tar.gz  5.2 MB 

Binaries  
Windows

coqinstaller8.5win32.exe (32 bits, bundled with CoqIDE, compiled using CoqSDK)  94 MB 
Windows

coqinstaller8.5win64.exe (64 bits, bundled with CoqIDE, compiled using CoqSDK 64 bits)  92 MB 
MacOS

CoqIDE_8.5.dmg (bundled with CoqIDE, compiled using OCaml 4.02.3 and Camlp5 6.14)  125 MB 
Documentation  
Tutorial.pdf  0.2 MB  
ReferenceManual.pdf (also online)  1.6 MB  
Standard Library online documentation 