From 2aa92f2da205db588734007f5d68cd1031bb83b5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Jul 2014 14:17:59 +0200
Subject: Documenting the change of semantics of the "constructor" tactic.

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

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
 
-- 
cgit v1.2.3