diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2015-01-14 14:04:02 +0100 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-01-14 14:50:58 +0100 |
commit | 5ec324ab5101be45c9cf9ffda9cbbbffde9b7df9 (patch) | |
tree | 0eb69496d39b8535384b5eaa535f8f8e9601b610 /doc/refman | |
parent | b63549edce71492617db99a75410256f1b0239b0 (diff) |
Reference manual: document multimatch.
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/RefMan-ltac.tex | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 494905f22..03facbdbb 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -127,6 +127,12 @@ is understood as {\tt lazymatch reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ & | & {\tt lazymatch} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\ +& | & +{\tt multimatch goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ +& | & +{\tt multimatch reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ +& | & +{\tt multimatch} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\ & | & {\tt abstract} {\atom}\\ & | & {\tt abstract} {\atom} {\tt using} {\ident} \\ & | & {\tt first [} \nelist{\tacexpr}{\tt |} {\tt ]}\\ @@ -703,6 +709,17 @@ it has backtracking points. \begin{Variants} +\item \index{multimatch!in Ltac} +\index{Ltac!multimatch} +Using {\tt multimatch} instead of {\tt match} will allow subsequent +tactics to backtrack into a right-hand side tactic which has +backtracking points left and trigger the selection of a new matching +branch when all the backtracking points of the right-hand side have +been consumed. + +The syntax {\tt match \ldots} is, in fact, a shorthand for +{\tt once multimatch \ldots}. + \item \index{lazymatch!in Ltac} \index{Ltac!lazymatch} Using {\tt lazymatch} instead of {\tt match} will perform the same @@ -816,6 +833,21 @@ first), but it possible to reverse this order (older first) with the {\tt match reverse goal with} variant. \variant + +\index{multimatch goal!in Ltac} +\index{Ltac!multimatch goal} +\index{multimatch reverse goal!in Ltac} +\index{Ltac!multimatch reverse goal} + +Using {\tt multimatch} instead of {\tt match} will allow subsequent +tactics to backtrack into a right-hand side tactic which has +backtracking points left and trigger the selection of a new matching +branch or combination of hypotheses when all the backtracking points +of the right-hand side have been consumed. + +The syntax {\tt match [reverse] goal \ldots} is, in fact, a shorthand for +{\tt once multimatch [reverse] goal \ldots}. + \index{lazymatch goal!in Ltac} \index{Ltac!lazymatch goal} \index{lazymatch reverse goal!in Ltac} |