From c2b0ca88cbc4e874e7b3bd9b9f4c07477cb5b530 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Jul 2014 17:47:15 +0200
Subject: Mentioning the incompatibility due to fixing bug #2996 (see #3418).

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

diff --git a/CHANGES b/CHANGES
index 6494173b58..fb1e839fe3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -120,6 +120,10 @@ Tactics
 - Tactic "subst id" now supports id occurring in dependent local definitions.
 - Bugs fixed about intro-pattern "*" might lead to some rare incompatibilities.
 - New tactical "time" to display time spent executing its argument.
+- Tactics referring or using a constant dependent in a section variable which
+  has been cleared or renamed in the current goal context now fail
+  (possible source of incompatibilities solvable by avoiding clearing
+  the relevant hypotheses).
 
 Program
 
-- 
cgit v1.2.3