Home

Coq 8.4pl4 is out

Submitted by boutillier on 12 May 2014 11:11 GMT

Version 8.4pl4 of Coq fixes several bugs of version 8.4pl3 including 3 critical ones. More information to be found in the CHANGES file.

WARNING: The current logic of Coq is now known to be inconsistent with Axiom prop_extensionality :
forall A B:Prop, (A <-> B) -> A = B.