diff options
| -rw-r--r-- | CHANGES | 10 |
1 files changed, 6 insertions, 4 deletions
@@ -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". |