Documentation de Show Intro(s)

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

1 files changed, 14 insertions, 0 deletions

diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index 669eee0dd..a1c189d91 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -286,6 +286,20 @@ are currently being proved.
 As it is possible to start proving a previous lemma during
 the proof of a theorem, this list may contain several 
 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
+writing of more robust scripts. For example, with an appropriate 
+Proof General macro, it is possible to transform any anonymous {\tt
+  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}.
+
 \end{Variants}
 
 \subsection{\tt Set Hyps\_limit {\num}.}