From bb37153d90de103dabd02285d11b3c39e3e4f89c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Jan 2015 21:48:12 +0100
Subject: Updating CHANGES (grammar, thanks to AS for pointing it out) + a line
 on "Intuition Negation Unfolding".

---
 CHANGES | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/CHANGES b/CHANGES
index 8c5b1c4a89..a8411a2126 100644
--- a/CHANGES
+++ b/CHANGES
@@ -120,7 +120,7 @@ Tactics
   * New tactics "revgoals", "cycle" and "swap" to reorder goals.
   * The semantics of recursive tactics (introduced with "Ltac t := ..."
     or "let rec t := ... in ...") changed slightly as t is now
-    applied to every goals, not each goal independently. In particular
+    applied to every goal, not each goal independently. In particular
     it may be applied when no goals are left. This may cause tactics
     such as "let rec t := constructor;t" to loop indefinitely. The
     simple fix is to rewrite the recursive calls as follows:
@@ -163,7 +163,9 @@ Tactics
   opposite side, new tactic "dtauto" is able to destruct any
   record-like inductive types, superseding the old version of "tauto".
 - Similarly, "intuition" has been made more uniform and, where it now
-  fails, "dintuition" can be used. (possible source of incompatibilities)
+  fails, "dintuition" can be used (possible source of incompatibilities).
+- New option "Unset Intuition Negation Unfolding" for deactivating automatic
+  unfolding of "not" in intuition.
 - Tactic notations can now be defined locally to a module (use "Local" prefix).
 - Tactic "red" now reduces head beta-iota redexes (potential source of
   rare incompatibilities).
-- 
cgit v1.2.3