eq fusionne avec eqT et devient par défaut sur Type,

idem pour ex et exT, ex2 et exT2, all et allT


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 61445214cd..7741ea4cf4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,10 @@ A revision of the standard library and of concrete syntax of Coq, including
 - renaming of various standard notions from French to English (esp in ZArith)
 - all notions of the standard library are declared with (strict)
   implicit arguments
+- eq merged with eqT: old eq disappear, new eq (written =) is old eqT
+  and new eqT is syntactic sugar for new eq (notation == is an alias
+  for = and is written as it)
+- similarly, ex, ex2 and all are merged with exT, exT2 and allT.
 
 Vernacular commands