From 317858b7ad05764a2ce010354631443f219a4b9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Dec 2015 12:03:45 +0100
Subject: Updating CHANGES with an incompatibility.

---
 CHANGES | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index 8cb5158753..b39d84ba57 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,7 +14,9 @@ Specification language
 Tactics
 
 - Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly
-  for induction.
+  for induction (rare source of incompatibilities easily solvable by
+  removing parentheses around "hyp" when not for the purpose of keeping
+  the hypothesis).
 - Syntax "p/c" for on-the-fly application of a lemma c before
   introducing along pattern p changed to p%c1..%cn. The feature and
   syntax are in experimental stage.
-- 
cgit v1.2.3