passe sur les labels et les refs dans chapitres tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8414 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 4 deletions

diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 6ac29e487..93b3d0f25 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -778,7 +778,7 @@ environment, provided that {\term} is well-typed.
     \texttt{Actually, it has type {\term$_3$}}.
 \end{ErrMsgs}
 
-\SeeAlso sections \ref{Opaque}, \ref{Transparent}, \ref{Unfold}
+\SeeAlso sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}
 
 \subsubsection{\tt Local {\ident} := {\term}.}\comindex{Local}
 This command binds the value {\term} to the name {\ident} in the
@@ -797,7 +797,7 @@ definition is a kind of {\em macro}.
 \end{Variants}
 
 \SeeAlso \ref{Section} (section mechanism), \ref{Opaque},
-\ref{Transparent} (opaque/transparent constants), \ref{Unfold}
+\ref{Transparent} (opaque/transparent constants), \ref{unfold}
 
 % Let comme forme de Definition n'existe plus
 %
@@ -962,7 +962,7 @@ equivalent to \\ {\tt Inductive {\ident} : {\sort} :=
       Same as before but with parameters.
 \end{Variants}
 
-\SeeAlso sections \ref{Cic-inductive-definitions}, \ref{Elim}
+\SeeAlso sections \ref{Cic-inductive-definitions}, \ref{elim}
 
 \subsubsection{Mutually inductive types}
 \comindex{Mutual Inductive}\label{Mutual-Inductive}
@@ -1366,7 +1366,7 @@ It is a synonymous of \texttt{Theorem}
 \item {\tt Definition {\ident} : {\type}.} \\
 Allow to define a term of type {\type} using the proof editing mode. It
 behaves as {\tt Theorem} except the defined term will be transparent (see
-\ref{Transparent}, \ref{Unfold}). 
+\ref{Transparent}, \ref{unfold}). 
 \end{Variants}
 
 \subsubsection{{\tt Proof} {\tt .} \dots {\tt Qed} {\tt .}}