aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--CHANGES4
1 files changed, 4 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index fb1e839fe3..6515d5d0f0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -124,6 +124,10 @@ Tactics
has been cleared or renamed in the current goal context now fail
(possible source of incompatibilities solvable by avoiding clearing
the relevant hypotheses).
+- Tactic "constructor" is now fully backtracking, thus deprecating the need of
+ the undocumented "contructor <tac>" syntax which is now equivalent to
+ "once (constructor; tac)". (potential source of rare incompatibilities).
+
Program