From 31ce6ad3ca351b4742f66ed059356191ae96a3ac Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 Jul 2015 19:16:05 +0200 Subject: Rewording about how to upgrade on failing calls to constructor. --- CHANGES | 10 ++++++---- 1 file 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 " 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 " 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". -- cgit v1.2.3