aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmi@gmail.com>2017-02-20 22:22:48 +0100
committerGravatar GitHub <noreply@github.com>2017-02-20 22:22:48 +0100
commit15e2280fe975fa5a4376ee45557d3e532e208496 (patch)
treea74b511ab69de96962732187ffb5b895243342cc /doc
parent278cebe6835512a5646eafcb13e1f020c0dc5d91 (diff)
Fix V7 syntax in refman.
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-pro.tex6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index c37367de5..16c822b6a 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -477,15 +477,15 @@ names.
\item{\tt Show Intro.}\comindex{Show Intro}\\
If the current goal begins by at least one product, this command
prints the name of the first product, as it would be generated by
-an anonymous {\tt Intro}. The aim of this command is to ease the
+an anonymous {\tt intro}. The aim of this command is to ease the
writing of more robust scripts. For example, with an appropriate
{\ProofGeneral} macro, it is possible to transform any anonymous {\tt
- Intro} into a qualified one such as {\tt Intro y13}.
+ intro} into a qualified one such as {\tt intro y13}.
In the case of a non-product goal, it prints nothing.
\item{\tt Show Intros.}\comindex{Show Intros}\\
This command is similar to the previous one, it simulates the naming
-process of an {\tt Intros}.
+process of an {\tt intros}.
\item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials}
\\ It displays