refman: avoid label names with whitespace (unsupported in html)

1 files changed, 4 insertions, 4 deletions

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}