1 files changed, 3 insertions, 1 deletions
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