Rewording about how to upgrade on failing calls to constructor.

1 files changed, 6 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 202e27e377..733bcc7cf5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -188,10 +188,12 @@ Tactics
     during the execution of c, it can backtrack and try b instead of a.
   * New tactical (once a) removes all the backtracking points from a
     (i.e. it selects the first success of a).
-  * Tactic "constructor" is now fully backtracking, thus deprecating
-    the need of the undocumented "constructor <tac>" syntax which is
-    now equivalent to "[> once (constructor; tac) ..]". (potential
-    source of rare incompatibilities).
+  * Tactic "constructor" is now fully backtracking. In case of
+    incompatibilities (e.g. combinatoric explosion), the former
+    behavior of "constructor" can be retrieved by using instead
+    "[> once constructor ..]". Thanks to backtracking, undocumented
+    "constructor <tac>" syntax is now equivalent to
+    "[> once (constructor; tac) ..]".
   * New "multimatch" variant of "match" tactic which backtracks to
     new branches in case of a later failure. The "match" tactic is
     equivalent to "once multimatch".