MAJ pour compilation coq-tex correcte

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

1 files changed, 5 insertions, 5 deletions

diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index 05156ba5f8..95de3ca78b 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -122,15 +122,15 @@ Consider the goal {\tt (R n p)} provable using the transitivity of
 Goal R n p.
 \end{coq_example*}
 
-The direct application of {\tt Rtrans} with {\tt Apply} fails because
-no value for {\tt y} in {\tt Rtrans} is found by {\tt Apply}:
+The direct application of {\tt Rtrans} with {\tt apply} fails because
+no value for {\tt y} in {\tt Rtrans} is found by {\tt apply}:
 
 \begin{coq_eval}
 Set Printing Depth 50.
+(********** The following is not correct and should produce **********)
+(**** Error: generated subgoal (R n ?17) has metavariables in it *****)
+(* Just to adjust the prompt: *) apply Rtrans.
 \end{coq_eval}
-% (********** The following is not correct and should produce **********)
-% (**** Error: generated subgoal (R n ?17) has metavariables in it *****)
-% (* Just to adjust the prompt: *) apply Rtrans.
 \begin{coq_example}
 apply Rtrans.
 \end{coq_example}