From ea452095b644373b5ba50272ba6a0087446421c3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 10 Apr 2002 11:29:38 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2625 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 26 +++++++++++++++++++++-----
 1 file changed, 21 insertions(+), 5 deletions(-)

diff --git a/CHANGES b/CHANGES
index 5b75441115..f95d9c5f54 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,29 +1,45 @@
 Changes from V7.2 to ????
 =========================
 
+Tactics
+
+- New tactic "Rename x into y" for renaming hypotheses
+- New tactics "Pose x:=u" and "Pose u" to add definitions to local context
+- Pattern now working on partially applied subterms
+- Ring no longer applies irreversible congruence laws of mult but
+  better applies congruence laws of plus (slight source of incompatibilities).
+- Intuition (cf JC)
+
 Bugs
 
 - "Intros H" now working like "Intro H" trying first to reduce if not a product
 - Forward dependencies in Cases now taken into account
 
+- Known bugs related to Inversion and let-in's fixed
+- Bug unexpected Delta with let-in now fixed
+
 Extraction (details in contrib/extraction/CHANGES or documentation)
 
-- Signatures of extracted terms are now mostly expunged from dummy arguments. 	
+- Signatures of extracted terms are now mostly expunged from dummy arguments.
 - Haskell extraction is now operational (tested & debugged).  
 
 Standard library
 
-- Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v and Zlogarithms.v)
-  moved from contrib/omega in order to be more visible, one Zsgn function, 
-  more induction principles (Wf_Z.v and tail of Zcomplements.v), 
-  one more general Euclid theorem. 
+- Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v
+  and Zlogarithms.v) moved from contrib/omega in order to be more
+  visible, one Zsgn function, more induction principles (Wf_Z.v and
+  tail of Zcomplements.v), one more general Euclid theorem.
 
 User Contributions
 
 - Chinese has been rewritten using Z from ZArith as datatype. 
   ZChinese is the new version, Chinese the obsolete one.   
 
+Incompatibilities
 
+- Ring: exceptional incompatibilities
+     (1 above 650 in submitted user contribs, leading to a simplification)
+- Intuition: ??
 
 
 Changes from V7.1 to V7.2
-- 
cgit v1.2.3