From 7bdfef00a00a6c7403166bcaadc9cdfcd0e92451 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 29 Mar 2003 16:47:26 +0000
Subject: 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
---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'CHANGES')

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
 
-- 
cgit v1.2.3