From 866d547fccecf9b07234a5933b3f0a835d179da2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 May 2002 10:18:01 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index d19cf2b095..41c2138ef3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,11 @@
 Changes from V7.2 to ????
 =========================
 
+Language
+
+- Slightly improved compilation of pattern-matching (slight source of
+  incompatibilities)
+
 Tactics
 
 - New tactic "Rename x into y" for renaming hypotheses
@@ -39,10 +44,13 @@ User Contributions
 
 Incompatibilities
 
-- Ring: exceptional incompatibilities
-     (1 above 650 in submitted user contribs, leading to a simplification)
+- Ring: exceptional incompatibilities (1 above 650 in submitted user
+  contribs, leading to a simplification)
 - Intuition: does not unfold any definition except "<->" and "~".
-
+- Cases: removal of some extra Cases in configurations of the form
+  "Cases ... of C _ => ... | _ D => ..."  (effects on 2 definitions of
+  submitted user contributions necessitating the removal of now superflous
+  proof steps in 3 different proofs)
 
 Changes from V7.1 to V7.2
 =========================
-- 
cgit v1.2.3