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 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/pptactic.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index d43b94ec4b..ddb85a3626 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -621,7 +621,10 @@ module Make | FullInversion -> primitive "inversion" | FullInversionClear -> primitive "inversion_clear" - let pr_lazy lz = if lz then keyword "lazy" else mt () + let pr_lazy = function + | General -> keyword "multi" + | Lazy -> keyword "lazy" + | Once -> mt () let pr_match_pattern pr_pat = function | Term a -> pr_pat a |