diff options
| author | Arnaud Spiwack | 2015-03-03 11:36:18 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-03-13 16:41:02 +0100 |
| commit | 17c1e778bc50ebb797e2b772bf72dbac403f9965 (patch) | |
| tree | f122d05835cd002f6b3436fccfe567accbc27854 | |
| parent | 9b8f5ef7125ed7b014521e1de7a40fb3905b0ae9 (diff) | |
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.
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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". |