From b7b17b4a587f83ce677848d33576ec1bd2b6074f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 14 May 2002 21:32:05 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index b1c7fee435..944db3dda7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,13 +24,15 @@ Tactics
   better applies congruence laws of plus (slight source of incompatibilities).
 - Intuition does no longer unfold constants except "<->" and "~". It
   can be parameterized by a tactic. It also can introduce dependent
-  product if needed.
+  product if needed
+- "Match Context" now matching more recent hypotheses first
+- "Match Context" now failing only on user errors and Fail tactic
+- Tactic Definition's without arguments now allowed in Coq states
 
 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
 
-- 
cgit v1.2.3