From 3d5a8667b566fbade7d0639b835ded2e1f8d53e4 Mon Sep 17 00:00:00 2001
From: glondu
Date: Tue, 5 Oct 2010 16:52:39 +0000
Subject: (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
---
 doc/refman/RefMan-ltac.tex | 9 ++++-----
 1 file 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
-- 
cgit v1.2.3