diff options
| author | herbelin | 2001-10-17 12:39:08 +0000 |
|---|---|---|
| committer | herbelin | 2001-10-17 12:39:08 +0000 |
| commit | 79757247806cffb089fab51ad6256d9e5142bbc2 (patch) | |
| tree | e0925f711fafacc5f1be154c28975eb42727e123 /doc/RefMan-pro.tex | |
| parent | 4fe518a1c458d7d6274ac1c1b2f97504e1652f56 (diff) | |
Corrections diverses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8250 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RefMan-pro.tex')
| -rwxr-xr-x | doc/RefMan-pro.tex | 2 |
1 files changed, 1 insertions, 1 deletions
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 |