From fd9bda79334608cfc2192d988d9eb074d81d6db3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 15 May 2002 10:05:16 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index 32e176beab..40604570ca 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,4 +1,4 @@
-Changes from V7.2 to ????
+Changes from V7.2 to V7.3
 =========================
 
 Language
@@ -25,8 +25,8 @@ Tactics
 - Intuition does no longer unfold constants except "<->" and "~". It
   can be parameterized by a tactic. It also can introduce dependent
   product if needed
-- "Match Context" now matching more recent hypotheses first
-- "Match Context" now failing only on user errors and Fail tactic
+- "Match Context" now matching more recent hypotheses first and failing only 
+  on user errors and Fail tactic (possible source of incompatibilities)
 - Tactic Definition's without arguments now allowed in Coq states
 
 Bugs
@@ -67,6 +67,9 @@ Incompatibilities
   "Cases ... of C _ => ... | _ D => ..."  (effects on 2 definitions of
   submitted user contributions necessitating the removal of now superflous
   proof steps in 3 different proofs)
+- Match Context, in case of incompatibilities because of a now non
+  trapped error (e.g. Not_found or Failure), use instead tactic Fail
+  to force Match Context trying the next clause
 
 Changes from V7.1 to V7.2
 =========================
-- 
cgit v1.2.3