aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-12-19 10:28:58 +0100
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-12-19 16:27:45 +0100
commitfb9815baafc008a6e67e542eb8c2adf7a6375fe8 (patch)
tree206244b9fb02320c8ab6b7c0381e9da4eaeb19b5 /Makefile.common
parenta07648ca9c6b06414b271632c620122e51bf0f4a (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 'Makefile.common')
0 files changed, 0 insertions, 0 deletions