Silence some warning about references in documentation.

5 files changed, 11 insertions, 11 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index c5cf41473f..a4ab671add 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -191,7 +191,7 @@ cannot appear in mutually inductive (or co-inductive) definitions.
   standard definitions.
 \item During the definition of the one-constructor inductive
   definition, all the errors of inductive definitions, as described in
-  Section~\ref{gal_Inductive_Definitions}, may also occur.
+  Section~\ref{gal-Inductive-Definitions}, may also occur.
 
 \end{ErrMsgs}
 
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index d043cda0f7..2f128abaa3 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -856,6 +856,7 @@ A formal presentation of constants and environments is given in
 Section~\ref{Typed-terms}.
 
 \subsubsection{\tt Definition {\ident} := {\term}.
+\label{Definition}
 \comindex{Definition}}
 
 This command binds {\term} to the name {\ident} in the
@@ -925,8 +926,8 @@ section and depending on {\ident} are prefixed by the let-in definition
 %% Inductive Types
 %%
 \subsection{Inductive definitions
-\index{Inductive definitions} 
-\label{gal_Inductive_Definitions}
+\index{Inductive definitions}
+\label{gal-Inductive-Definitions}
 \comindex{Inductive}
 \label{Inductive}}
 
@@ -1283,7 +1284,7 @@ CoInductive Stream : Set :=
 \end{coq_example}
 
 The syntax of this command is the same as the command \texttt{Inductive}
-(see Section~\ref{gal_Inductive_Definitions}). Notice that no
+(see Section~\ref{gal-Inductive-Definitions}). Notice that no
 principle of induction is derived from the definition of a
 co-inductive type, since such principles only make sense for inductive
 ones. For co-inductive ones, the only elimination principle is case
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 13b2d387b8..c924c02ebe 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -27,7 +27,7 @@ problems.
 \def\cpattern{\nterm{cpattern}}
 
 The syntax of the tactic language is given Figures~\ref{ltac}
-and~\ref{ltac_aux}. See Chapter~\ref{BNF-syntax} for a description of
+and~\ref{ltac-aux}. See Chapter~\ref{BNF-syntax} for a description of
 the BNF metasyntax used in these grammar rules. Various already
 defined entries will be used in this chapter: entries
 {\naturalnumber}, {\integer}, {\ident}, {\qualid}, {\term},
@@ -187,7 +187,7 @@ is understood as
 \end{tabular}
 \end{centerframe}
 \caption{Syntax of the tactic language (continued)}
-\label{ltac_aux}
+\label{ltac-aux}
 \end{figure}
 
 \begin{figure}[ht]
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 096f4cae45..399ea8f99c 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -45,7 +45,7 @@ A tactic is applied as an ordinary command. It may be preceded by a
 goal selector: {\tt all} if the tactic is to be applied to every
 focused goal simultaneously, or a natural number $n$ if it is to be
 applied to the $n$-th goal. If no selector is specified, the default
-selector (see Section \ref{default_selector}) is used.
+selector (see Section \ref{default-selector}) is used.
 
 \newcommand{\selector}{\nterm{selector}}
 \begin{tabular}{lcl}
@@ -56,7 +56,7 @@ selector (see Section \ref{default_selector}) is used.
 \subsection[\tt Set Default Goal Selector ``\selector''.]
            {\tt Set Default Goal Selector ``\selector''.
             \comindex{Set Default Goal Selector}
-            \label{default_selector}}
+            \label{default-selector}}
 After using this command, the default selector -- used when no selector
 is specified when applying a tactic -- is set to the chosen value. The
 initial value is $1$, hence the tactics are, by default, applied to
@@ -2734,7 +2734,7 @@ Lemmas are added to the database using the command
 
 The tactic is especially useful for parametric setoids which are not
 accepted as regular setoids for {\tt rewrite} and {\tt
-  setoid\_replace} (see Chapter~\ref{setoid_replace}).
+  setoid\_replace} (see Chapter~\ref{setoids}).
 
 \begin{Variants}
 \item{\tt stepl {\term} by {\tac}}
@@ -3699,7 +3699,6 @@ development.
 
 \subsection{\tt Remove Hints \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$
   \mbox{\dots} \ident$_m$}
-\label{PrintHint}
 \comindex{Remove Hints}
 
 This command removes the hints associated to terms \term$_1$ \mbox{\dots}
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 8a293ea2bf..55915189ce 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -2,7 +2,7 @@
 
 \achapter{\protect{Generalized rewriting}}
 \aauthor{Matthieu Sozeau}
-\label{setoid_replace}
+\label{setoids}
 
 This chapter presents the extension of several equality related tactics
 to work over user-defined structures (called setoids) that are equipped