diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 36 |
2 files changed, 7 insertions, 32 deletions
@@ -143,6 +143,9 @@ Tactics refine, use (refine c;shelve_unifiable). This can still cause incompatibilities in rare occasions. * New "give_up" tactic to skip over a goal without admitting it. +- Matching using "lazymatch" was fundamentally modified. It now behaves + like "match" (immediate execution of the matching branch) but without + the backtracking mechanism in case of failure. - New "cbn" tactic, a well-behaved simpl. - Repeated identical calls to omega should now produce identical proof terms. - Tactics btauto, a reflexive Boolean tautology solver. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 7e6c0bd123..6f26c5eebf 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -686,14 +686,8 @@ then a no-matching-clause error is raised. \item \index{lazymatch!in Ltac} \index{Ltac!lazymatch} -Using {\tt lazymatch} instead of {\tt match} has an effect if the -right-hand-side of a clause returns a tactic. With {\tt match}, the -tactic is applied to the current goal (and the next clause is tried if -it fails). With {\tt lazymatch}, the tactic is directly returned as -the result of the whole {\tt lazymatch} block without being first -tried to be applied to the goal. Typically, if the {\tt lazymatch} -block is bound to some variable $x$ in a {\tt let in}, then tactic -expression gets bound to the variable $x$. +Using {\tt lazymatch} instead of {\tt match} disables the backtracking +mechanism. \item \index{context!in pattern} There is a special form of patterns to match a subterm against the @@ -799,30 +793,8 @@ the {\tt match reverse goal with} variant. \index{Ltac!lazymatch goal} \index{lazymatch reverse goal!in Ltac} \index{Ltac!lazymatch reverse goal} -Using {\tt lazymatch} instead of {\tt match} has an effect if the -right-hand-side of a clause returns a tactic. With {\tt match}, the -tactic is applied to the current goal (and the next clause is tried if -it fails). With {\tt lazymatch}, the tactic is directly returned as -the result of the whole {\tt lazymatch} block without being first -tried to be applied to the goal. Typically, if the {\tt lazymatch} -block is bound to some variable $x$ in a {\tt let in}, then tactic -expression gets bound to the variable $x$. - -\begin{coq_example} -Ltac test_lazy := - lazymatch goal with - | _ => idtac "here"; fail - | _ => idtac "wasn't lazy"; trivial - end. -Ltac test_eager := - match goal with - | _ => idtac "here"; fail - | _ => idtac "wasn't lazy"; trivial - end. -Goal True. -test_lazy || idtac "was lazy". -test_eager || idtac "was lazy". -\end{coq_example} +Using {\tt lazymatch} instead of {\tt match} disables the backtracking +mechanism. \subsubsection[Filling a term context]{Filling a term context\index{context!in expression}} |