From 9d5e80b3478964e0e40c139a75b8ef4013efabcf Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 14 Jan 2015 12:00:24 +0100
Subject: Reference manual: try and improve the documentation of lazymatch.

In particular try to avoid the use of the word "backtracking" which refers to too many things.
---
 doc/refman/RefMan-ltac.tex | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index dbb71a4142..95467acd7f 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -701,8 +701,12 @@ then a no-matching-clause error is raised.
 
 \item \index{lazymatch!in Ltac}
 \index{Ltac!lazymatch}
-Using {\tt lazymatch} instead of {\tt match} disables the backtracking
-mechanism.
+Using {\tt lazymatch} instead of {\tt match} will perform the same
+pattern matching procedure but will commit to the first matching
+branch rather than trying a new matching if the right-hand side
+fails. If the right-hand side of the selected branch is a tactic with
+backtracking points, then subsequent failures cause this tactic to
+backtrack.
 
 \item \index{context!in pattern}
 There is a special form of patterns to match a subterm against the
@@ -808,8 +812,12 @@ 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} disables the backtracking
-mechanism.
+Using {\tt lazymatch} instead of {\tt match} will perform the same
+pattern matching procedure but will commit to the first matching
+branch with the first matching combination of hypotheses rather than
+trying a new matching if the right-hand side fails. If the right-hand
+side of the selected branch is a tactic with backtracking points, then
+subsequent failures cause this tactic to backtrack.
 
 \subsubsection[Filling a term context]{Filling a term context\index{context!in expression}}
 
-- 
cgit v1.2.3