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 /dev | |
| 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 'dev')
0 files changed, 0 insertions, 0 deletions