diff options
Diffstat (limited to 'doc/refman/RefMan-oth.tex')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 4 |
1 files changed, 2 insertions, 2 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 |