diff options
| -rwxr-xr-x | doc/RefMan-pro.tex | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex index 669eee0ddf..a1c189d914 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}.} |