From ec0ae1070f15a3bc8a6f6699500b146ecd69dec3 Mon Sep 17 00:00:00 2001
From: courant
Date: Fri, 12 Apr 2002 13:37:08 +0000
Subject: *** empty log message ***

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

diff --git a/CHANGES b/CHANGES
index f95d9c5f54..0315275b1e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,7 +8,9 @@ Tactics
 - 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)
+- Intuition does no longer unfold constants except "<->" and "~". It
+  can be parameterized by a tactic. It also can introduce dependent
+  product if needed.
 
 Bugs
 
-- 
cgit v1.2.3