diff options
| author | Arnaud Spiwack | 2014-12-19 10:28:58 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-19 16:27:45 +0100 |
| commit | fb9815baafc008a6e67e542eb8c2adf7a6375fe8 (patch) | |
| tree | 206244b9fb02320c8ab6b7c0381e9da4eaeb19b5 /parsing | |
| parent | a07648ca9c6b06414b271632c620122e51bf0f4a (diff) | |
Add a backtracking version of Ltac's [match].
[multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index b2b1d5adea..fa2c111a68 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -172,7 +172,9 @@ GEXTEND Gram | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; match_key: - [ [ "match" -> false | "lazymatch" -> true ] ] + [ [ "match" -> Once + | "lazymatch" -> Lazy + | "multimatch" -> General ] ] ; input_fun: [ [ "_" -> None |