From 79757247806cffb089fab51ad6256d9e5142bbc2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Oct 2001 12:39:08 +0000
Subject: Corrections diverses

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8250 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-pro.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/RefMan-pro.tex')

diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index a1c189d914..03f01d8d7d 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -251,7 +251,7 @@ This command displays the current goals.
   Displays the whole list of tactics applied from the beginning
   of the current proof. 
   This tactics script may contain some holes (subgoals not yet proved).
-  They are printed as \verb!<Your Tactic Text here>!.
+  They are printed under the form \verb!<Your Tactic Text here>!.
 
 \item {\tt Show Tree.}\comindex{Show Tree}\\
 This command can be seen as a more structured way of
-- 
cgit v1.2.3