diff options
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 9 |
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 |