(Hopefully) clearer explanation of Ltac's context patterns

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13503 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 5 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index ec9776de98..090bbb0a92 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -553,11 +553,10 @@ pattern:
 \begin{quote}
 {\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}
 \end{quote}
-It matches any term which one subterm matches {\cpattern}. If there is
-a match, the optional {\ident} is assign the ``matched context'', that
-is the initial term where the matched subterm is replaced by a
-hole. The definition of {\tt context} in expressions below will show
-how to use such term contexts.
+It matches any term with a subterm matching {\cpattern}. If there is
+a match, the optional {\ident} is assigned the ``matched context'', i.e.
+the initial term where the matched subterm is replaced by a
+hole. The example below will show how to use such term contexts.
 
 If the evaluation of the right-hand-side of a valid match fails, the
 next matching subterm is tried. If no further subterm matches, the