Documenting the change of semantics of the "constructor" tactic.

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