diff options
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-oth.tex | 4 | ||||
-rw-r--r-- | doc/refman/RefMan-tac.tex | 8 |
2 files changed, 6 insertions, 6 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index dc5143fd1..121b608d0 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -971,7 +971,7 @@ This command displays the current nesting depth used for display. %Not yet documented. \section{Controlling the reduction strategies and the conversion algorithm} -\label{Controlling reduction strategy} +\label{Controlling_reduction_strategy} {\Coq} provides reduction strategies that the tactics can invoke and two different algorithms to check the convertibility of types. @@ -1170,7 +1170,7 @@ control the scope of their effect. There are four kinds of commands: outside the sections and modules they occurs in. The {\tt Transparent} and {\tt Opaque} (see - Section~\ref{Controlling reduction strategy}) commands belong to + Section~\ref{Controlling_reduction_strategy}) commands belong to this category. \item Commands whose default behavior is to extend their effect diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 5c87b12cc..e05ed721a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -106,7 +106,7 @@ different forms: \end{itemize} \subsection{Occurrences sets and occurrences clauses} -\label{Occurrences clauses} +\label{Occurrences_clauses} \index{Occurrences clauses} An occurrences clause is a modifier to some tactics that obeys the @@ -1103,7 +1103,7 @@ matching the pattern. This notation allows specifying which occurrences of {\term} have to be substituted in the context. The {\tt in {\occgoalset}} clause is an occurrence clause whose syntax and behavior are described in -Section~\ref{Occurrences clauses}. +Section~\ref{Occurrences_clauses}. \item {\tt set ( {\ident} \nelistnosep{\binder} := {\term} )} @@ -1606,7 +1606,7 @@ syntax {\tt destruct ({\num})} (not very interesting anyway). This syntax is used for selecting which occurrences of {\term} the case analysis has to be done on. The {\tt in {\occgoalset}} clause is an occurrence clause whose syntax and behavior is described in - Section~\ref{Occurrences clauses}. + Section~\ref{Occurrences_clauses}. \item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} @@ -1791,7 +1791,7 @@ induction n. This syntax is used for selecting which occurrences of {\term} the induction has to be carried on. The {\tt in \occgoalset} clause is an occurrence clause whose syntax and behavior is described in - Section~\ref{Occurrences clauses}. + Section~\ref{Occurrences_clauses}. \item {\tt induction {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} %% eqn:{\namingintropattern} |