From 17c1e778bc50ebb797e2b772bf72dbac403f9965 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 3 Mar 2015 11:36:18 +0100
Subject: CHANGES: more correct equivalent to "constructor tac" syntax.

As mentionne in #3969, using "once (constructor;tac)" leads in exponential blowups, whereas "[> once (constructor;tac) ..]" does not.
---
 CHANGES | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGES b/CHANGES
index 5b3043fdfe..19683f8e39 100644
--- a/CHANGES
+++ b/CHANGES
@@ -112,8 +112,8 @@ Tactics
     (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).
+    now equivalent to "[> once (constructor; tac) ..]". (potential
+    source of rare incompatibilities).
   * 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".
-- 
cgit v1.2.3