diff options
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index e292013db..1a004b665 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -291,7 +291,7 @@ subgoals which clutter your screen. \begin{Variant} \item {\tt Focus {\num}.}\\ -This focuses the attention on the $\num^{\scriptsize th}$ subgoal to prove. +This focuses the attention on the $\num^{th}$ subgoal to prove. \end{Variant} @@ -379,7 +379,7 @@ along with the type and the context of each variable. \end{Variants} -\subsection[\tt Guarded.] +\subsection[\tt Guarded.]{\tt Guarded.\comindex{Guarded}\label{Guarded}} Some tactics (e.g. refine \ref{refine}) allow to build proofs using fixpoint or co-fixpoint constructions. Due to the incremental nature |