Standardisation du format des références croisées vers Figure, Section, Chapter

Remplacement pageref par ref parce que pageref n'a pas de sens pour
la version HTML



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

20 files changed, 150 insertions, 149 deletions

diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 345608c6f..a0f483ab0 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -11,7 +11,7 @@
 This section describes the full form of pattern-matching in {\Coq} terms.
 
 \asection{Patterns}\label{implementation} The full syntax of {\tt
-match} is presented in figures~\ref{term-syntax}
+match} is presented in Figures~\ref{term-syntax}
 and~\ref{term-syntax-aux}.  Identifiers in patterns are either
 constructor names or variables. Any identifier that is not the
 constructor of an inductive or coinductive type is considered to be a
@@ -472,7 +472,7 @@ In all the previous examples the elimination predicate does not depend
 on the object(s) matched. But it may depend and the typical case 
 is when we write a proof by induction or a function that yields an
 object of dependent type. An example of proof using \texttt{match} in
-given in section \ref{refine-example}
+given in Section~\ref{refine-example}
 
 For example, we can write 
 the function \texttt{buildlist} that given a natural number
@@ -524,7 +524,7 @@ the second is not.
 % $[\vec{d_1}:\vec{D_1}][x_1:T_1]\ldots [\vec{d_n}:\vec{D_n}][x_n:T_n]Q.$
 
 The user can also use \texttt{match} in combination with the tactic
-\texttt{refine} (see section \ref{refine}) to build incomplete proofs
+\texttt{refine} (see Section~\ref{refine}) to build incomplete proofs
 beginning with a \texttt{match} construction.
 
 \asection{Pattern-matching on inductive objects involving local
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index 5445224b0..b4bae4235 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -327,7 +327,7 @@ By default, a coercion is never printed.
 \index{Coercions!and records}
 We allow the definition of {\em Structures with Inheritance} (or
 classes as records) by extending the existing {\tt Record} macro
-(see section~\ref{Record}). Its new syntax is:
+(see Section~\ref{Record}). Its new syntax is:
 
 \begin{center}
 \begin{tabular}{l}
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index c8daea1dc..da9b3e717 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -182,7 +182,7 @@ this constant is not declared in the generated file.
 \asubsection{Realizing axioms}\label{extraction:axioms}
 
 Extraction will fail if it encounters an informative
-axiom not realized (see section \ref{extraction:axioms}). 
+axiom not realized (see Section~\ref{extraction:axioms}). 
 A warning will be issued if it encounters an logical axiom, to remind 
 user that inconsistant logical axioms may lead to incorrect or 
 non-terminating extracted terms. 
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 6c30e23fc..0d9422dd9 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -14,7 +14,7 @@
 We present here the new \Program\ tactic commands, used to build certified
 \Coq\ programs, elaborating them from their algorithmic skeleton and a
 rich specification \cite{Sozeau06}. It can be sought of as a dual of extraction
-(chapter \ref{Extraction}). The goal of \Program~is to program as in a regular
+(see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular
 functional programming language whilst using as rich a specification as 
 desired and proving that the code meets the specification using the whole \Coq{} proof
 apparatus. This is done using a technique originating from the
@@ -44,7 +44,7 @@ generate an obligation for every such coercion. In the other direction,
 
 Another distinction is the treatment of pattern-matching. Apart from the
 following differences, it is equivalent to the standard {\tt match}
-operation (section \ref{Caseexpr}).
+operation (see Section~\ref{Caseexpr}).
 \begin{itemize}
 \item Generation of equalities. A {\tt match} expression is always
   generalized by the corresponding equality. As an example,
@@ -82,7 +82,7 @@ fall back directly to \Coq's usual typing of dependent pattern-matching.
 
 
 The next two commands are similar to their standard counterparts
-Definition (section \ref{Simpl-definitions}) and Fixpoint (section \ref{Fixpoint}) in that
+Definition (see Section~\ref{Simpl-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that
 they define constants. However, they may require the user to prove some
 goals to construct the final definitions.
 
@@ -129,7 +129,7 @@ obligations. Once solved using the commands shown below, it binds the final
   \label{ProgramFixpoint}}
 
 The structural fixpoint operator behaves just like the one of Coq
-(section \ref{Fixpoint}), except it may also generate obligations.
+(see Section~\ref{Fixpoint}), except it may also generate obligations.
 It works with mutually recursive definitions too.
 
 \begin{coq_example}
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 7759b8055..dc7235ae6 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -16,7 +16,7 @@ We call this calculus the
 {\em Predicative Calculus of (Co)Inductive
   Constructions}\index{Predicative Calculus of
   (Co)Inductive Constructions} (\pCIC\ in short).
-In section~\ref{impredicativity} we give the extra-rules for \iCIC. A
+In Section~\ref{impredicativity} we give the extra-rules for \iCIC. A
   compiling option of \Coq{} allows to type-check theories in this
   extended system.
 
@@ -28,7 +28,7 @@ type.  For instance, the statement {\it ``for all x, P''} is not
 allowed in type theory; you must say instead: {\it ``for all x
 belonging to T, P''}. The expression {\it ``x belonging to T''} is
 written {\it ``x:T''}. One also says: {\it ``x has type T''}.
-The terms of {\CIC} are detailed in section \ref{Terms}.
+The terms of {\CIC} are detailed in Section~\ref{Terms}.
 
 In \CIC\, there is an internal reduction mechanism. In particular, it
 allows to decide if two programs are {\em intentionally} equal (one
@@ -132,7 +132,7 @@ the universe variables is maintained globally. To ensure the existence
 of a mapping of the universes to the positive integers, the graph of
 constraints must remain acyclic.  Typing expressions that violate the
 acyclicity of the graph of constraints results in a \errindex{Universe
-inconsistency} error (see also section~\ref{PrintingUniverses}).
+inconsistency} error (see also Section~\ref{PrintingUniverses}).
 
 \subsection{Constants}
 Besides the sorts, the language also contains constants denoting
@@ -266,7 +266,7 @@ names. Declarations are either assumptions or ``standard''
 definitions, that is abbreviations for well-formed terms
 but also definitions of inductive objects. In the latter
 case, an object in the environment will define one or more constants
-(that is types and constructors, see section \ref{Cic-inductive-definitions}).
+(that is types and constructors, see Section~\ref{Cic-inductive-definitions}).
 
 An assumption will be represented in the environment as
 \Assum{\Gamma}{c}{T} which means that $c$ is assumed of some type $T$
@@ -346,7 +346,7 @@ be derived from the following rules.
 \Rem We may have $\kw{let}~x:=t~\kw{in}~u$
 well-typed without having $((\lb~x:T\mto u)~t)$ well-typed (where
 $T$ is a type of $t$). This is because the value $t$ associated to $x$
-may be used in a conversion rule (see section \ref{conv-rules}).
+may be used in a conversion rule (see Section~\ref{conv-rules}).
 
 \section[Conversion rules]{Conversion rules\index{Conversion rules}
 \label{conv-rules}}
@@ -372,7 +372,7 @@ refer the interested reader to \cite{Coq85}.
 
 \paragraph[$\iota$-reduction.]{$\iota$-reduction.\label{iota}\index{iota-reduction@$\iota$-reduction}}
 A specific conversion rule is associated to the inductive objects in
-the environment.  We shall give later on (section \ref{iotared}) the
+the environment.  We shall give later on (see Section~\ref{iotared}) the
 precise rules but it just says that a destructor applied to an object
 built from a constructor behaves as expected.  This reduction is
 called $\iota$-reduction and is more precisely studied in
@@ -455,7 +455,7 @@ convertibility rule of \Coq.
 A term which cannot be any more reduced is said to be in {\em normal
   form}. There are several ways (or strategies) to apply the reduction
 rule. Among them, we have to mention the {\em head reduction} which
-will play an important role (see chapter \ref{Tactics}). Any term can
+will play an important role (see Chapter~\ref{Tactics}). Any term can
 be written as $\lb~x_1:T_1\mto \ldots \lb x_k:T_k \mto 
 (t_0\ t_1\ldots t_n)$ where
 $t_0$ is not an application. We say then that $t_0$ is the {\em head
@@ -995,7 +995,7 @@ inductive types (i.e. of inductive types with one single constructor
 and that contains either proofs or inhabitants of singleton types
 only). More precisely, a small singleton inductive family is set in
 {\Prop}, a small non singleton inductive family is set in {\Set} (even
-in case {\Set} is impredicative -- see section~\ref{impredicativity}),
+in case {\Set} is impredicative -- see Section~\ref{impredicativity}),
 and otherwise in the {\Type} hierarchy.
 % TODO: clarify the case of a partial application ??
 
@@ -1529,7 +1529,7 @@ The terms structurally smaller than $y$ are:
   which one of the $I_l$ occurs) are structurally smaller than $y$.
 \end{itemize}
 The following definitions are correct, we enter them using the
-{\tt Fixpoint} command as described in section~\ref{Fixpoint} and show
+{\tt Fixpoint} command as described in Section~\ref{Fixpoint} and show
 the internal representation.
 \begin{coq_example}
 Fixpoint plus (n m:nat) {struct n} : nat :=
@@ -1630,14 +1630,14 @@ Abort.
 \subsubsection{Mutual induction}
 
 The principles of mutual induction can be automatically generated 
-using the {\tt Scheme} command described in section~\ref{Scheme}.
+using the {\tt Scheme} command described in Section~\ref{Scheme}.
 
 \section{Coinductive types}
 The implementation contains also coinductive definitions, which are
 types inhabited by infinite objects. 
 More information on coinductive definitions can be found
 in~\cite{Gimenez95b,Gim98,GimCas05}.
-%They are described in chapter~\ref{Coinductives}.
+%They are described in Chapter~\ref{Coinductives}.
 
 \section[\iCIC : the Calculus of Inductive Construction with
   impredicative \Set]{\iCIC : the Calculus of Inductive Construction with
diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex
index 7de837436..2c0396642 100644
--- a/doc/refman/RefMan-coi.tex
+++ b/doc/refman/RefMan-coi.tex
@@ -157,7 +157,7 @@ CoFixpoint zeros  : Stream nat := cons nat 0%N zeros.
 CoFixpoint from (n:nat) : Stream nat := cons nat n (from (S n)).
 \end{coq_example}
 
-As in the \verb!Fixpoint! command (cf. section~\ref{Fixpoint}), it is possible 
+As in the \verb!Fixpoint! command (see Section~\ref{Fixpoint}), it is possible 
 to introduce a block of mutually dependent methods. The general syntax
 for this case is :
 
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index a35f12aa6..845ef7889 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -34,7 +34,7 @@ the Caml toplevel with the command \verb!Drop.!, and come back to the
 \Coq~toplevel with the command \verb!Toplevel.loop();;!.
 
 % The command \verb!coqtop -searchisos! runs the search tool {\sf
-%   Coq\_SearchIsos} (see section~\ref{coqsearchisos},
+%   Coq\_SearchIsos} (see Section~\ref{coqsearchisos},
 % page~\pageref{coqsearchisos}) and, as the \Coq~system, can be combined
 % with the option \verb!-opt!.
 
@@ -44,7 +44,7 @@ looks for a vernacular file named {\em file}{\tt .v}, and tries to
 compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}).
 
 \Warning The name {\em file} must be a regular {\Coq} identifier, as
-defined in the section \ref{lexical}. It
+defined in the Section~\ref{lexical}. It
 must only contain letters, digits or underscores
 (\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be
 \verb+/bar/foo/to-to.v+ . 
@@ -240,7 +240,7 @@ The following command-line options are recognized by the commands {\tt
 \item[{\tt -vm}]\ 
 
   This activates the use of the bytecode-based conversion algorithm
-  for the current session (see section~\ref{SetVirtualMachine}).
+  for the current session (see Section~\ref{SetVirtualMachine}).
 
 \item[{\tt -image} {\em file}]\ 
 
@@ -272,7 +272,7 @@ The following command-line options are recognized by the commands {\tt
 % \begin{description}
 % \item[{\tt -searchisos}]\ \\
 %   Launch the {\sf Coq\_SearchIsos} toplevel
-%   (see section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}).
+%   (see Section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}).
 % \end{description}
 
 % $Id$ 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index f6e44f91a..31a1eabb2 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -9,7 +9,7 @@ the Gallina's syntax.
 
 The \verb+Record+ construction is a macro allowing the definition of
 records as is done in many programming languages.  Its syntax is
-described on figure \ref{record-syntax}.  In fact, the \verb+Record+
+described on Figure~\ref{record-syntax}.  In fact, the \verb+Record+
 macro is more general than the usual record types, since it allows
 also for ``manifest'' expressions. In this sense, the \verb+Record+
 construction allows to define ``signatures''.
@@ -231,7 +231,7 @@ construction defined using the extended {\tt match} is generally
 printed under its expanded form (see~\texttt{Set Printing Matching} in
 section~\ref{SetPrintingMatching}).
 
-\SeeAlso chapter \ref{Mult-match-full}.
+\SeeAlso Chapter~\ref{Mult-match-full}.
 
 \subsection{Pattern-matching on boolean values: the {\tt if} expression
 \label{if-then-else}
@@ -283,7 +283,7 @@ Check (fun x (H:{x=0}+{x<>0}) =>
 \end{coq_example}
 
 Notice that the printing uses the {\tt if} syntax because {\tt sumbool} is
-declared as such (see section \ref{printing-options}).
+declared as such (see Section~\ref{printing-options}).
 
 \subsection{Irrefutable patterns: the destructuring {\tt let}
 \index{let in@{\tt let ... in}}
@@ -521,7 +521,7 @@ Print fst.
 % Fix} implementing a combinator for primitive recursion equivalent to
 % the {\tt Match} construction of \Coq\ V5.8. It is provided only for
 % sake of compatibility with \Coq\ V5.8. It is recommended to avoid it.
-% (see section~\ref{Matchexpr}).
+% (see Section~\ref{Matchexpr}).
 
 % There is also a notation \texttt{Case} that is the
 % ancestor of \texttt{match}. Again, it is still in the code for
@@ -542,7 +542,7 @@ Print fst.
 %% It forces the first term to be of type the second term. The
 %% type must be compatible with
 %% the term. More precisely it must be either a type convertible to
-%% the automatically inferred type (see chapter \ref{Cic}) or a type
+%% the automatically inferred type (see Chapter~\ref{Cic}) or a type
 %% coercible to it, (see \ref{Coercions}). When the type of a
 %% whole expression is forced, it is usually not necessary to give the types of
 %% the variables involved in the term.
@@ -581,9 +581,9 @@ The {\tt Function} construction enjoys also the {\tt with} extension
 to define mutually recursive definitions. However, this feature does
 not work for non structural recursive functions. % VRAI??
 
-See the documentation of {\tt functional induction} (section
-\ref{FunInduction}) and {\tt Functional Scheme} (section
-\ref{FunScheme} and \ref{FunScheme-examples}) for how to use the 
+See the documentation of {\tt functional induction}
+(see Section~\ref{FunInduction}) and {\tt Functional Scheme}
+(see Section~\ref{FunScheme} and \ref{FunScheme-examples}) for how to use the
 induction principle to easily reason about the function.
 
 \noindent {\bf Remark: } To obtain the right principle, it is better
@@ -803,7 +803,7 @@ inside section {\tt s1} and outside.
 \item Most commands, like {\tt Hint}, {\tt Notation}, option management, ...
 which appear inside a section are cancelled when the
 section is closed.
-% cf section \ref{LongNames}
+% see Section~\ref{LongNames}
 %\item Usually all identifiers must be distinct. 
 %However, a name already used in a closed section (see \ref{Section})
 %can be reused. In this case, the old name is no longer accessible.
@@ -1234,7 +1234,7 @@ Conversely, to restore the hidding of implicit arguments, use command
 {\tt Unset Printing Implicit.}
 \end{quote}
 
-\SeeAlso {\tt Set Printing All} in section \ref{SetPrintingAll}.
+\SeeAlso {\tt Set Printing All} in Section~\ref{SetPrintingAll}.
 
 \subsection{Interaction with subtyping}
 
@@ -1377,14 +1377,14 @@ which declares the construction denoted by {\qualid} as a
 coercion between {\class$_1$} and {\class$_2$}.
 
 More details and examples, and a description of the commands related
-to coercions are provided in chapter \ref{Coercions-full}.
+to coercions are provided in Chapter~\ref{Coercions-full}.
 
 \section[Printing constructions in full]{Printing constructions in full\label{SetPrintingAll}
 \comindex{Set Printing All}
 \comindex{Unset Printing All}}
 
 Coercions, implicit arguments, the type of pattern-matching, but also
-notations (see chapter \ref{Addoc-syntax}) can obfuscate the behavior
+notations (see Chapter~\ref{Addoc-syntax}) can obfuscate the behavior
 of some tactics (typically the tactics applying to occurrences of
 subterms are sensitive to the implicit arguments). The command
 \begin{quote}
@@ -1411,7 +1411,7 @@ The following command:
 {\tt Set Printing Universes}
 \end{quote}
 activates the display of the actual level of each occurrence of
-{\Type}. See section~\ref{Sorts} for details.  This wizard option, in
+{\Type}. See Section~\ref{Sorts} for details.  This wizard option, in
 combination with \texttt{Set Printing All} (see
 section~\ref{SetPrintingAll}) can help to diagnose failures to unify
 terms apparently identical but internally different in the Calculus of
@@ -1424,7 +1424,7 @@ of the occurrences of {\Type}, use
 \comindex{Print Universes}
 
 The constraints on the internal level of the occurrences of {\Type}
-(see section~\ref{Sorts}) can be printed using the command
+(see Section~\ref{Sorts}) can be printed using the command
 \begin{quote}
 {\tt Print Universes.}
 \end{quote}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 8ee30b8fb..23c19d60b 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1,21 +1,22 @@
 \chapter{The \gallina{} specification language
 \label{Gallina}\index{Gallina}}
+\label{BNF-syntax} % Used referred to as a chapter label
 
 This chapter describes \gallina, the specification language of {\Coq}.
 It allows to develop mathematical theories and to prove specifications
 of programs.  The theories are built from axioms, hypotheses,
 parameters, lemmas, theorems and definitions of constants, functions,
 predicates and sets. The syntax of logical objects involved in
-theories is described in section \ref{term}. The language of
+theories is described in Section~\ref{term}. The language of
 commands, called {\em The Vernacular} is described in section
 \ref{Vernacular}.
 
 In {\Coq}, logical objects are typed to ensure their logical
 correctness. The rules implemented by the typing algorithm are described in
-chapter \ref{Cic}.
+Chapter \ref{Cic}.
 
 \subsection*{About the grammars in the manual
-\label{BNF-syntax}\index{BNF metasyntax}}
+\index{BNF metasyntax}}
 
 Grammars are presented in Backus-Naur form (BNF). Terminal symbols are
 set in {\tt typewriter font}.  In addition, there are special
@@ -219,9 +220,9 @@ possible one (among all tokens defined at this moment), and so on.
 Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic
 set of terms which form the {\em Calculus of Inductive Constructions}
 (also called \CIC). The formal presentation of {\CIC} is given in
-chapter \ref{Cic}. Extensions of this syntax are given in chapter
+Chapter \ref{Cic}. Extensions of this syntax are given in chapter
 \ref{Gallina-extension}. How to customize the syntax is described in
-chapter \ref{Addoc-syntax}.
+Chapter \ref{Addoc-syntax}.
 
 \begin{figure}[htbp]
 \begin{centerframe}
@@ -363,7 +364,7 @@ denote local {\em variables}, what qualified identifiers do not.
 
 Numerals have no definite semantics in the calculus. They are mere
 notations that can be bound to objects through the notation mechanism
-(see chapter~\ref{Addoc-syntax} for details). Initially, numerals are
+(see Chapter~\ref{Addoc-syntax} for details). Initially, numerals are
 bound to Peano's representation of natural numbers
 (see~\ref{libnats}).
 
@@ -393,7 +394,7 @@ subclass of the syntactic class {\term}.
 \index{specif@{\specif}}
 \item {\Type} is the type of {\Set} and {\Prop}
 \end{itemize}
-\noindent More on sorts can be found in section \ref{Sorts}.
+\noindent More on sorts can be found in Section~\ref{Sorts}.
 
 \bigskip
 
@@ -596,10 +597,10 @@ Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false)
 \end{coq_example*}
 
 The second subcase is only relevant for annotated inductive types such
-as the equality predicate (see section~\ref{Equality}), the order
-predicate on natural numbers % (see section~\ref{le}) % undefined reference
+as the equality predicate (see Section~\ref{Equality}), the order
+predicate on natural numbers % (see Section~\ref{le}) % undefined reference
 or the type of
-lists of a given length (see section~\ref{listn}). In this configuration,
+lists of a given length (see Section~\ref{listn}). In this configuration,
 the type of each branch can depend on the type dependencies specific
 to the branch and the whole pattern-matching expression has a type
 determined by the specific dependencies in the type of the term being
@@ -1271,7 +1272,7 @@ CoInductive Stream : Set :=
 \end{coq_example}
 
 The syntax of this command is the same as the command \texttt{Inductive}
-(cf. 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
@@ -1525,7 +1526,7 @@ Eval compute in (tl (from 0)).
      with\\
         \mbox{}\hspace{0.1cm} $\ldots$  \\
         with {\ident$_m$}   : {\type$_m$} := {\term$_m$}}\\
-As in the \texttt{Fixpoint} command (cf. Section~\ref{Fixpoint}), it
+As in the \texttt{Fixpoint} command (see Section~\ref{Fixpoint}), it
 is possible to introduce a block of mutually dependent methods.
 \end{Variants}
 
@@ -1536,7 +1537,7 @@ is possible to introduce a block of mutually dependent methods.
 
 A statement claims a goal of which the proof is then interactively done
 using tactics. More on the proof editing mode, statements and proofs can be
-found in chapter \ref{Proof-handling}.
+found in Chapter~\ref{Proof-handling}.
 
 \subsubsection{\tt Theorem {\ident} : {\type}.
 \comindex{Theorem}
@@ -1586,7 +1587,7 @@ A proof starts by the keyword {\tt Proof}.  Then {\Coq} enters the
 proof editing mode until the proof is completed. The proof editing
 mode essentially contains tactics that are described in chapter
 \ref{Tactics}. Besides tactics, there are commands to manage the proof
-editing mode. They are described in chapter \ref{Proof-handling}. When
+editing mode. They are described in Chapter~\ref{Proof-handling}. When
 the proof is completed it should be validated and put in the
 environment using the keyword {\tt Qed}.
 \medskip
diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex
index ecb872b0e..23006b72e 100644
--- a/doc/refman/RefMan-ind.tex
+++ b/doc/refman/RefMan-ind.tex
@@ -18,7 +18,7 @@ macro-generate complicated uses of the basic elimination tactics for
 inductive types. 
 
 Sections \ref{inversion_introduction} to \ref{inversion_using}  present
-inversion tactics and section \ref{scheme} describes
+inversion tactics and Section~\ref{scheme} describes
 a command {\tt Scheme} for automatic generation of induction schemes
 for mutual inductive types.
 
diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex
index c93d7217f..14b14ae57 100644
--- a/doc/refman/RefMan-int.tex
+++ b/doc/refman/RefMan-int.tex
@@ -48,7 +48,7 @@ commands are processed from a file.
   the {\tt coqc} command from the operating system. 
 
 \end{itemize}
-These two modes are documented in chapter \ref{Addoc-coqc}.
+These two modes are documented in Chapter~\ref{Addoc-coqc}.
 
 Other modes of interaction with \Coq{} are possible: through an emacs
 shell window, an emacs generic user-interface for proof assistant
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index f1913d7cc..33c68e49d 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -12,12 +12,12 @@ The \Coq\ library is structured into three parts:
   various developments of \Coq\ axiomatizations about sets, lists,
   sorting, arithmetic, etc. This library comes with the system and its
   modules are directly accessible through the \verb!Require! command
-  (see section~\ref{Require});
+  (see Section~\ref{Require});
 
 \item[User contributions:] Other specification and proof developments
   coming from the \Coq\ users' community. These libraries are
   available for download at \texttt{http://coq.inria.fr} (see
-  section~\ref{Contributions}).
+  Section~\ref{Contributions}).
 \end{description}
 
 This chapter briefly reviews these libraries.
@@ -112,7 +112,7 @@ The basic library of {\Coq} comes with the definitions of standard
 (intuitionistic) logical connectives (they are defined as inductive
 constructions). They are equipped with an appealing syntax enriching the
 (subclass {\form}) of the syntactic class {\term}. The syntax
-extension is shown on figure \ref{formulas-syntax}.
+extension is shown on Figure~\ref{formulas-syntax}.
 
 % The basic library of {\Coq} comes with the definitions of standard
 % (intuitionistic) logical connectives (they are defined as inductive
@@ -819,7 +819,7 @@ subdirectories:
 These directories belong to the initial load path of the system, and
 the modules they provide are compiled at installation time. So they
 are directly accessible with the command \verb!Require! (see
-chapter~\ref{Other-commands}). 
+Chapter~\ref{Other-commands}). 
 
 The different modules of the \Coq\ standard library are described in the
 additional document \verb!Library.dvi!. They are also accessible on the WWW
@@ -828,7 +828,7 @@ through the \Coq\ homepage
 
 \subsection[Notations for integer arithmetics]{Notations for integer arithmetics\index{Arithmetical notations}}
 
-On figure \ref{zarith-syntax} is described the syntax of expressions
+On Figure~\ref{zarith-syntax} is described the syntax of expressions
 for integer arithmetics. It is provided by requiring and opening the
 module {\tt ZArith} and opening scope {\tt Z\_scope}.
 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 467a47346..48d27a50a 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -27,14 +27,14 @@ problems.
 \def\cpattern{\nterm{cpattern}}
 
 The syntax of the tactic language is given Figures~\ref{ltac}
-and~\ref{ltac_aux}. See page~\pageref{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},
 {\cpattern} and {\atomictac} represent respectively the natural and
 integer numbers, the authorized identificators and qualified names,
 {\Coq}'s terms and patterns and all the atomic tactics described in
-chapter~\ref{Tactics}. The syntax of {\cpattern} is the same as that
+Chapter~\ref{Tactics}. The syntax of {\cpattern} is the same as that
 of terms, but it is extended with pattern matching metavariables. In
 {\cpattern}, a pattern-matching metavariable is represented with the
 syntax {\tt ?id} where {\tt id} is a {\ident}. The notation {\tt \_}
@@ -536,7 +536,7 @@ If the evaluation of the right-hand-side of a valid match fails, the
 next matching subterm is tried. If no further subterm matches, the
 next clause is tried. Matching subterms are considered top-bottom and
 from left to right (with respect to the raw printing obtained by
-setting option {\tt Printing All}, see section~\ref{SetPrintingAll}).
+setting option {\tt Printing All}, see Section~\ref{SetPrintingAll}).
 
 \begin{coq_example}
 Ltac f x :=
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 4df212f9e..63e43dd7d 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -64,14 +64,14 @@ the resulting term with its type. The term to be reduced may depend on
 hypothesis introduced in the first subgoal (if a proof is in
 progress).
 
-\SeeAlso section~\ref{Conversion-tactics}.
+\SeeAlso Section~\ref{Conversion-tactics}.
 
 \subsection[\tt Extraction \term.]{\tt Extraction \term.\label{ExtractionTerm}
 \comindex{Extraction}} 
 This command displays the extracted term from
 {\term}. The extraction is processed according to the distinction
 between {\Set} and {\Prop}; that is to say, between logical and
-computational content (see section \ref{Sorts}). The extracted term is
+computational content (see Section~\ref{Sorts}). The extracted term is
 displayed in Objective Caml syntax, where global identifiers are still
 displayed as in \Coq\ terms.
 
@@ -81,7 +81,7 @@ displayed as in \Coq\ terms.
   globals {\qualid$_1$} \ldots{} {\qualid$_n$}.
 \end{Variants}
 
-\SeeAlso chapter~\ref{Extraction}.
+\SeeAlso Chapter~\ref{Extraction}.
 
 \subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} This command tells not to unfold the
 the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using
@@ -161,7 +161,7 @@ This restricts the search to constructions not defined in modules
 
 \begin{ErrMsgs}
 \item \errindex{Module/section \module{} not found}
-No module \module{} has been required (see section~\ref{Require}).
+No module \module{} has been required (see Section~\ref{Require}).
 \end{ErrMsgs}
 
 \end{Variants}
@@ -425,7 +425,7 @@ for \Coq's toplevel. This kind of file is called a {\em script} for
 \subsection[\tt Load {\ident}.]{\tt Load {\ident}.\comindex{Load}\label{Load}}
 This command loads the file named {\ident}{\tt .v}, searching
 successively in each of the directories specified in the {\em
-  loadpath}. (see section \ref{loadpath})
+  loadpath}. (see Section~\ref{loadpath})
 
 \begin{Variants}
 \item {\tt Load {\str}.}\label{Load-str}\\
@@ -439,7 +439,7 @@ successively in each of the directories specified in the {\em
   \comindex{Load Verbose}
   Display, while loading, the answers of \Coq\ to each command
   (including tactics) contained in the loaded file
-  \SeeAlso section \ref{Begin-Silent}
+  \SeeAlso Section~\ref{Begin-Silent}
 \end{Variants}
 
 \begin{ErrMsgs}
@@ -572,7 +572,7 @@ These different variants can be combined.
 
   The command did not find the file {\tt toto.vo}. Either {\tt
     toto.v} exists but is not compiled or {\tt toto.vo} is in a directory
-  which is not in your {\tt LoadPath} (see section \ref{loadpath}).
+  which is not in your {\tt LoadPath} (see Section~\ref{loadpath}).
 
 \item \errindex{Bad magic number}
 
@@ -582,7 +582,7 @@ These different variants can be combined.
   version of \Coq.
 \end{ErrMsgs}
 
-\SeeAlso chapter \ref{Addoc-coqc}
+\SeeAlso Chapter~\ref{Addoc-coqc}
 
 \subsection[\tt Print Modules.]{\tt Print Modules.\comindex{Print Modules}}
 This command shows the currently loaded and currently opened
@@ -592,10 +592,10 @@ This command shows the currently loaded and currently opened
 This commands loads the Objective Caml compiled files {\str$_1$} \dots
 {\str$_n$} (dynamic link). It is mainly used to load tactics
 dynamically.
-% (see chapter \ref{WritingTactics}).
+% (see Chapter~\ref{WritingTactics}).
  The files are
 searched into the current Objective Caml loadpath (see the command {\tt
-Add ML Path} in the section \ref{loadpath}).  Loading of Objective Caml
+Add ML Path} in the Section~\ref{loadpath}).  Loading of Objective Caml
 files is only possible under the bytecode version of {\tt coqtop}
 (i.e. {\tt coqtop} called with options {\tt -byte}, see chapter 
 \ref{Addoc-coqc}).
@@ -608,14 +608,14 @@ files is only possible under the bytecode version of {\tt coqtop}
 \subsection[\tt Print ML Modules.]{\tt Print ML Modules.\comindex{Print ML Modules}}
 This print the name of all \ocaml{} modules loaded with \texttt{Declare
   ML Module}. To know from where these module were loaded, the user
-should use the command \texttt{Locate File} (see page \pageref{Locate File})
+should use the command \texttt{Locate File} (see Section~\ref{Locate File})
 
 \section[Loadpath]{Loadpath\label{loadpath}\index{Loadpath}}
 
 There are currently two loadpaths in \Coq. A loadpath where seeking
 {\Coq} files (extensions {\tt .v} or {\tt .vo} or {\tt .vi}) and one where
 seeking Objective Caml files. The default loadpath contains the
-directory ``\texttt{.}'' denoting the current directory and mapped to the empty logical path (see section \ref{LongNames}).
+directory ``\texttt{.}'' denoting the current directory and mapped to the empty logical path (see Section~\ref{LongNames}).
 
 \subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}}
 This command displays the current working directory.
@@ -662,14 +662,14 @@ This command displays the current \Coq\ loadpath.
 
 \subsection[\tt Add ML Path {\str}.]{\tt Add ML Path {\str}.\comindex{Add ML Path}}
 This command adds the path {\str} to the current Objective Caml loadpath (see
-the command {\tt Declare ML Module} in the section \ref{compiled}).
+the command {\tt Declare ML Module} in the Section~\ref{compiled}).
 
 \Rem This command is implied by {\tt Add LoadPath {\str} as {\dirpath}}.
 
 \subsection[\tt Add Rec ML Path {\str}.]{\tt Add Rec ML Path {\str}.\comindex{Add Rec ML Path}}
 This command adds the directory {\str} and all its subdirectories 
 to the current Objective Caml loadpath (see
-the command {\tt Declare ML Module} in the section \ref{compiled}).
+the command {\tt Declare ML Module} in the Section~\ref{compiled}).
 
 \Rem This command is implied by {\tt Add Rec LoadPath {\str} as {\dirpath}}.
 
@@ -727,15 +727,15 @@ This command is dedicated for the use in graphical interfaces.  It
 allows to backtrack to a particular \emph{global} state, i.e.
 typically a state corresponding to a previous line in a script. A
 global state includes declaration environment but also proof
-environment (see chapter~\ref{Proof-handling}). The three numbers
+environment (see Chapter~\ref{Proof-handling}). The three numbers
 $\num_1$, $\num_2$ and $\num_3$ represent the following:
 \begin{itemize}
 \item $\num_3$: Number of \texttt{Abort} to perform, i.e. the number
   of currently opened nested proofs that must be cancelled (see
-  chapter~\ref{Proof-handling}).
+  Chapter~\ref{Proof-handling}).
 \item $\num_2$: \emph{Proof state number} to unbury once aborts have
   been done. Coq will compute the number of \texttt{Undo} to perform
-  (see chapter~\ref{Proof-handling}).
+  (see Chapter~\ref{Proof-handling}).
 \item $\num_1$: Environment state number to unbury, Coq will compute
   the number of \texttt{Back} to perform.
 \end{itemize}
@@ -758,7 +758,7 @@ Where:
 \begin{itemize}
 \item \emph{$id_i$} is the name of the current proof (if there is
   one, otherwise \texttt{Coq} is displayed, see
-chapter~\ref{Proof-handling}).
+Chapter~\ref{Proof-handling}).
 \item $\num_1$ is the environment state number after the last
   command.
 \item $\num_2$ is the proof state number after the last
@@ -814,7 +814,7 @@ use in a further session. This file can be given as the {\tt
 \begin{Variants}
 \item {\tt Write State \ident}\\
  Equivalent to {\tt Write State "}{\ident}{\tt .coq"}.
- The state is saved in the current directory (see \pageref{Pwd}).
+ The state is saved in the current directory (see Section~\ref{Pwd}).
 \end{Variants}
 
 \section{Quitting and debugging}
@@ -840,7 +840,7 @@ all abstract types of \Coq - section\_path, identfifiers, terms, judgements,
 \dots. You can also use the file \texttt{base\_include} instead,
 that loads only the pretty-printers for section\_paths and
 identifiers.
-% See section \ref{test-and-debug} more information on the
+% See Section~\ref{test-and-debug} more information on the
 % usage of the toplevel.
 You can return back to \Coq{} with the command: 
 
@@ -851,9 +851,9 @@ go();;
 \end{flushleft}
 
 \begin{Warnings}
-\item It only works with the bytecode version of {\Coq} (i.e. {\tt coqtop} called with option {\tt -byte}, see page \pageref{binary-images}).
+\item It only works with the bytecode version of {\Coq} (i.e. {\tt coqtop} called with option {\tt -byte}, see the contents of Section~\ref{binary-images}).
 \item You must have compiled {\Coq} from the source package and set the
-  environment variable \texttt{COQTOP} to the root of your copy of the sources (see section \ref{EnvVariables}).
+  environment variable \texttt{COQTOP} to the root of your copy of the sources (see Section~\ref{EnvVariables}).
 \end{Warnings}
 
 \subsection[\tt Time \textrm{\textsl{command}}.]{\tt Time \textrm{\textsl{command}}.\comindex{Time}
@@ -907,7 +907,7 @@ This command displays the current nesting depth used for display.
 \section{Controlling the conversion algorithm}
 
 {\Coq} comes with two algorithms to check the convertibility of types
-(see section~\ref{convertibility}). The first algorithm lazily
+(see Section~\ref{convertibility}). The first algorithm lazily
 compares applicative terms while the other is a brute-force but efficient
 algorithm that first normalizes the terms before comparing them.  The
 second algorithm is based on a bytecode representation of terms
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 1a004b665..d0ca09747 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -2,12 +2,12 @@
 \label{Proof-handling}}
 
 In \Coq's proof editing mode all top-level commands documented in 
-chapter \ref{Vernacular-commands} remain available
+Chapter~\ref{Vernacular-commands} remain available
 and the user has access to specialized commands dealing with proof
 development pragmas documented in this section. He can also use some
 other specialized commands called {\em tactics}.  They are the very
 tools allowing the user to deal with logical reasoning. They are
-documented in chapter \ref{Tactics}.\\ 
+documented in Chapter~\ref{Tactics}.\\ 
 When switching in editing proof mode, the prompt
 \index{Prompt} 
 {\tt Coq <} is changed into {\tt {\ident} <} where {\ident} is the
@@ -21,7 +21,7 @@ generated by the tactics.
 To each subgoal is associated  a number of
 hypotheses we call the {\em \index*{local context}} of the goal.
 Initially, the local context is empty. It is enriched by the use of
-certain tactics (see mainly section~\ref{intro}).
+certain tactics (see mainly Section~\ref{intro}).
 
 When a proof is achieved the message {\tt Proof completed} is
 displayed. One can then store this proof as a defined constant in the
@@ -54,7 +54,7 @@ that goal.
 %the command {\tt Goal} cannot be used while a proof is already being edited.
 \end{ErrMsgs}
 
-\SeeAlso section \ref{Theorem}
+\SeeAlso Section~\ref{Theorem}
 
 \subsection[\tt Qed.]{\tt Qed.\comindex{Qed}\label{Qed}}
 This command is available in interactive editing proof mode when the
@@ -117,7 +117,7 @@ This command switches to interactive editing proof mode and declares
 as a {\tt Theorem}, the name {\ident} is known at all section levels:
 {\tt Theorem} is a {\sl global} lemma.
 
-%\ErrMsg (see section \ref{Goal})
+%\ErrMsg (see Section~\ref{Goal})
 
 \begin{ErrMsgs}
 
@@ -164,7 +164,7 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels:
 \label{BeginProof}}
 This command applies in proof editing mode. It is equivalent to {\tt
   exact {\term}; Save.} That is, you have to give the full proof in
-one gulp, as a proof term (see section \ref{exact}).
+one gulp, as a proof term (see Section~\ref{exact}).
 
 \variant {\tt Proof.}
   
@@ -173,7 +173,7 @@ one gulp, as a proof term (see section \ref{exact}).
   practice to use {\tt Proof.} as an opening parenthesis, closed in
   the script with a closing {\tt Qed.}
 
-\SeeAlso {\tt Proof with {\tac}.} in section~\ref{ProofWith}.
+\SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}.
 
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
@@ -232,14 +232,14 @@ This commands switches back to the editing of the last edited proof.
 
 This command allows to instantiate an existential variable. {\tt \num}
 is an index in the list of uninstantiated existential variables
-displayed by {\tt Show Existentials.} (described in section~\ref{Show})
+displayed by {\tt Show Existentials.} (described in Section~\ref{Show})
 
 This command is intented to be used to instantiate existential
 variables when the proof is completed but some uninstantiated
 existential variables remain. To instantiate existential variables
 during proof edition, you should use the tactic {\tt instantiate}.
 
-\SeeAlso {\tt instantiate (\num:= \term).} in section~\ref{instantiate}.
+\SeeAlso {\tt instantiate (\num:= \term).} in Section~\ref{instantiate}.
 
 
 %%%%%%%%
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 9bde8c490..583e4406c 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -7,13 +7,13 @@ commands are {\tt Notation} and {\tt Infix} which are described in
 section \ref{Notation}.  It also happens that the same symbolic
 notation is expected in different contexts. To achieve this form of
 overloading, {\Coq} offers a notion of interpretation scope. This is
-described in section \ref{scopes}.
+described in Section~\ref{scopes}.
 
 \Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which
 were present for a while in {\Coq} are no longer available from {\Coq}
 version 8.0. The underlying AST structure is also no longer available.
 The functionalities of the command {\tt Syntactic Definition} are
-still available, see section \ref{Abbreviations}.
+still available, see Section~\ref{Abbreviations}.
 
 \section[Notations]{Notations\label{Notation}
 \comindex{Notation}}
@@ -209,7 +209,7 @@ Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level).
 For the sake of factorization with {\Coq} predefined rules, simple
 rules have to be observed for notations starting with a symbol:
 e.g. rules starting with ``\{'' or ``('' should be put at level 0. The
-list of {\Coq} predefined notations can be found in chapter \ref{Theories}.
+list of {\Coq} predefined notations can be found in Chapter~\ref{Theories}.
 
 The command to display the current state of the {\Coq} term parser is
 \comindex{Print Grammar constr}
@@ -374,7 +374,7 @@ and corecursive definitions can benefit of customized notations. To do
 this, insert a {\tt where} notation clause after the definition of the
 (co)inductive type or (co)recursive term (or after the definition of
 each of them in case of mutual definitions). The exact syntax is given
-on Figure \ref{notation-syntax}. Here are examples:
+on Figure~\ref{notation-syntax}. Here are examples:
 
 \begin{coq_eval}
 Set Printing Depth 50.
@@ -418,7 +418,7 @@ To reactivate it, use the command
 \end{quote}
 The default is to use notations for printing terms wherever possible.
 
-\SeeAlso {\tt Set Printing All} in section \ref{SetPrintingAll}.
+\SeeAlso {\tt Set Printing All} in Section~\ref{SetPrintingAll}.
 
 \subsection{Locating notations
 \comindex{Locate}
@@ -597,8 +597,8 @@ a single identifier.
 \paragraph{Syntax of notations}
 
 The different syntactic variants of the command \texttt{Notation} are
-given on Figure \ref{notation-syntax}. The optional {\tt :{\scope}} is
-described in the section \ref{scopes}.
+given on Figure~\ref{notation-syntax}. The optional {\tt :{\scope}} is
+described in the Section~\ref{scopes}.
 
 \Rem No typing of the denoted expression is performed at definition
 time. Type-checking is done only at the time of use of the notation.
@@ -743,7 +743,7 @@ is interpreted in the scope stack extended by the scopes bound (if any)
 to these arguments.
 
 \SeeAlso The command to show the scopes bound to the arguments of a
-function is described in section \ref{About}.
+function is described in Section~\ref{About}.
 
 \subsubsection{Binding types of arguments to an interpretation scope}
 
@@ -759,7 +759,7 @@ interpretation of the notation itself expects arguments of the same
 type that would trigger the same scope).
 
 \comindex{Bind Scope}
-More generally, any {\class} (see chapter \ref{Coercions-full}) can be
+More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be
 bound to an interpretation scope. The command to do it is
 \begin{quote}
 {\tt Bind Scope} {\scope} \texttt{with} {\class}
@@ -782,7 +782,7 @@ Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))).
 interpretation. See the next section.
 
 \SeeAlso The command to show the scopes bound to the arguments of a
-function is described in section \ref{About}.
+function is described in Section~\ref{About}.
 
 \subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope}}
 
@@ -878,7 +878,7 @@ This includes the notation for pairs. It is delimited by key {\tt core}.
 
 This includes notation for strings as elements of the type {\tt
 string}.  Special characters and escaping follow {\Coq} conventions
-on strings (see page~\pageref{strings}). Especially, there is no
+on strings (see Section~\ref{strings}). Especially, there is no
 convention to visualize non printable characters of a string.  The
 file {\tt String.v} shows an example that contains quotes, a newline
 and a beep (i.e. the ascii character of code 7).
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 335cc3f15..6276b547b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -33,7 +33,7 @@ satisfied. If it is not the case, the tactic raises an error message.
 Tactics are build from atomic tactics and tactic expressions (which
 extends the folklore notion of tactical) to combine those atomic
 tactics. This chapter is devoted to atomic tactics. The tactic
-language will be described in chapter~\ref{TacticLanguage}.
+language will be described in Chapter~\ref{TacticLanguage}.
 
 There are, at least, three levels of atomic tactics. The simplest one
 implements basic rules of the logical framework. The second level is
@@ -98,7 +98,7 @@ holes. The holes are noted ``\texttt{\_}''.
   which type cannot be inferred. Put a cast around it.
 \end{ErrMsgs}
 
-An example of use is given in section~\ref{refine-example}.
+An example of use is given in Section~\ref{refine-example}.
 
 \section{Basics
 \index{Typing rules}}
@@ -348,7 +348,7 @@ match the current goal against the conclusion of the type of {\term}.
 If it succeeds, then the tactic returns as many subgoals as the number
 of non dependent premises of the type of {\term}.  The tactic {\tt
 apply} relies on first-order pattern-matching with dependent
-types. See {\tt pattern} in section \ref{pattern} to transform a
+types. See {\tt pattern} in Section~\ref{pattern} to transform a
 second-order pattern-matching problem into a first-order one.
 
 \begin{ErrMsgs}
@@ -581,7 +581,7 @@ in the list of subgoals remaining to prove.
 %    \vref$_n$ := \term$_n$}
 %  \tacindex{Specialize \dots\ with} \\ 
 %  It is to provide the tactic with some explicit values to instantiate
-%  premises of {\term} (see section \ref{Binding-list}).
+%  premises of {\term} (see Section~\ref{Binding-list}).
 %  Some other premises are inferred using type information and
 %  unification. The resulting well-formed 
 %  term being {\tt (\term~\term'$_1$\dots\term'$_k$)}
@@ -685,7 +685,7 @@ to $T$.
 \label{change}}
 
 This tactic applies to any goal. It implements the rule
-``Conv''\index{Typing rules!Conv} given in section~\ref{Conv}.  {\tt
+``Conv''\index{Typing rules!Conv} given in Section~\ref{Conv}.  {\tt
   change U} replaces the current goal \T\ with \U\ providing that
 \U\ is well-formed and that \T\ and \U\ are convertible.
 
@@ -739,7 +739,7 @@ product {\tt \ident$_i$:T} (for some type \T); if \vref$_i$ is
 A bindings list can also be a simple list of terms {\tt \term$_1$
   \term$_2$ \dots\term$_n$}. In that case the references to which
 these terms correspond are determined by the tactic. In case of {\tt
-  elim} (see section~\ref{elim}) the terms should correspond to
+  elim} (see Section~\ref{elim}) the terms should correspond to
 all the dependent products in the type of \term\ while in the case of
 {\tt apply} only the dependent products which are not bound in
 the conclusion of the type are given.
@@ -943,7 +943,7 @@ product or an applicative term in head normal form or a variable.
 The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}.
 
 \Rem The $\delta$ rule only applies to transparent constants
-(see section~\ref{Opaque} on transparency and opacity).
+(see Section~\ref{Opaque} on transparency and opacity).
 
 \subsection{\tt simpl
 \tacindex{simpl}}
@@ -1575,7 +1575,7 @@ Qed.
 \item {\tt decompose record \term}\tacindex{decompose record}
   This decomposes record types (inductive types with one constructor,
   like \texttt{and} and \texttt{exists} and those defined with the
-  \texttt{Record} macro, see p.~\pageref{Record}).
+  \texttt{Record} macro, see Section~\ref{Record}).
 \end{Variants}
 
 
@@ -1586,8 +1586,8 @@ Qed.
 The \emph{experimental} tactic \texttt{functional induction} performs
 case analysis and induction following the definition of a function. It
 makes use of a principle generated by \texttt{Function}
-(section~\ref{Function}) or \texttt{Functional Scheme}
-(section~\ref{FunScheme}).
+(see Section~\ref{Function}) or \texttt{Functional Scheme}
+(see Section~\ref{FunScheme}).
 
 \begin{coq_eval}
 Reset Initial.
@@ -1613,15 +1613,15 @@ you want to write implicit arguments explicitly.
 \Rem \texttt{functional induction (f x1 x2 x3)} is actually a wrapper
 for \texttt{induction x1 x2 x3 (f x1 x2 x3) using \qualid} followed by
 a cleaning phase, where $\qualid$ is the induction principle
-registered for $f$ (by the \texttt{Function} (section~\ref{Function})
-or \texttt{Functional Scheme} (section~\ref{FunScheme}) command)
+registered for $f$ (by the \texttt{Function} (see Section~\ref{Function})
+or \texttt{Functional Scheme} (see Section~\ref{FunScheme}) command)
 corresponding to the sort of the goal.  Therefore \texttt{functional
   induction} may fail if the induction scheme (\texttt{\qualid}) is
-not defined. See also section~\ref{Function} for the function terms
+not defined. See also Section~\ref{Function} for the function terms
 accepted by \texttt{Function}.
 
 \Rem There is a difference between obtaining an induction scheme for a
-function by using \texttt{Function} (section~\ref{Function}) and by
+function by using \texttt{Function} (see Section~\ref{Function}) and by
 using \texttt{Functional Scheme} after a normal definition using
 \texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
 details.
@@ -1642,7 +1642,7 @@ details.
    using \term$_{m+1}$ with {\term$_{n+1}$} \dots {\term$_m$}}
 
  Similar to \texttt{Induction} and \texttt{elim}
- (section~\ref{Tac-induction}), allows to give explicitly the
+ (see Section~\ref{Tac-induction}), allows to give explicitly the
  induction principle and the values of dependent premises of the
  elimination scheme, including \emph{predicates} for mutual induction
  when \qualid is mutually recursive.
@@ -1652,11 +1652,11 @@ details.
     {\vref$_m$} := {\term$_n$}}
 
   Similar to \texttt{induction} and \texttt{elim}
-  (section~\ref{Tac-induction}).
+  (see Section~\ref{Tac-induction}).
 
 \item All previous variants can be extended by the usual \texttt{as
     \intropattern} construction, similarly for example to
-  \texttt{induction} and \texttt{elim} (section~\ref{Tac-induction}).
+  \texttt{induction} and \texttt{elim} (see Section~\ref{Tac-induction}).
     
 \end{Variants}
 
@@ -1857,7 +1857,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{setoid_replace}).
 
 \tacindex{stepr}
 \comindex{Declare Right Step}
@@ -2350,7 +2350,7 @@ the instance with the tactic {\tt inversion}.
 which performs inversion on hypothesis \ident\ of the form
 \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ =
   \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been
-defined using \texttt{Function} (section~\ref{Function}).
+defined using \texttt{Function} (see Section~\ref{Function}).
 
 \begin{ErrMsgs}
 \item \errindex{Hypothesis \ident must contain at least one Function}
@@ -2590,7 +2590,7 @@ and then uses {\tt auto} which completes the proof.
 
 Originally due to C{\'e}sar~Mu{\~n}oz, these tactics ({\tt tauto} and {\tt intuition})
 have been completely reengineered by David~Delahaye using mainly the tactic
-language (see chapter~\ref{TacticLanguage}). The code is now quite shorter and
+language (see Chapter~\ref{TacticLanguage}). The code is now quite shorter and
 a significant increase in performances has been noticed. The general behavior
 with respect to dependent types, unfolding and introductions has
 slightly changed to get clearer semantics. This may lead to some
@@ -2742,7 +2742,7 @@ vernacular command.
 % \item {\tt Linear with \ident$_1$ \dots\ \ident$_n$}\\
 %   \tacindex{Linear with} 
 %   Is equivalent to apply first {\tt generalize \ident$_1$ \dots
-%     \ident$_n$} (see section \ref{generalize}) then the \texttt{Linear}
+%     \ident$_n$} (see Section~\ref{generalize}) then the \texttt{Linear}
 %   tactic.  So one can use axioms, lemmas or hypotheses of the local
 %   context with \texttt{Linear} in this way.
 % \end{Variants}
@@ -2840,7 +2840,7 @@ formulas built with \verb|~|, \verb|\/|, \verb|/\|,
 both the type \texttt{nat} of natural numbers and \texttt{Z} of binary
 integers. This tactic must be loaded by the command \texttt{Require Import
   Omega}. See the additional documentation about \texttt{omega}
-(chapter~\ref{OmegaChapter}).
+(see Chapter~\ref{OmegaChapter}).
 
 \subsection{{\tt ring} and {\tt ring\_simplify \term$_1$ \dots\ \term$_n$}
 \tacindex{ring}
@@ -2859,7 +2859,7 @@ the terms given in the conclusion of the goal by their normal
 forms. If no term is given, then the conclusion should be an equation
 and both hand sides are normalized.
 
-See chapter~\ref{ring} for more information on the tactic and how to
+See Chapter~\ref{ring} for more information on the tactic and how to
 declare new ring structures.
 
 \subsection{{\tt field}, {\tt field\_simplify \term$_1$\dots\ \term$_n$}
@@ -2885,7 +2885,7 @@ division nor inverse.
 All of these 3 tactics may generate a subgoal in order to prove that
 denominators are different from zero.
 
-See chapter~\ref{ring} for more information on the tactic and how to
+See Chapter~\ref{ring} for more information on the tactic and how to
 declare new field structures.
 
 \Example
@@ -2973,9 +2973,9 @@ $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
 
 \end{Variant}
 
-\SeeAlso section \ref{HintRewrite} for feeding the database of lemmas used by {\tt autorewrite}.
+\SeeAlso Section~\ref{HintRewrite} for feeding the database of lemmas used by {\tt autorewrite}.
 
-\SeeAlso section \ref{autorewrite-example} for examples showing the use of
+\SeeAlso Section~\ref{autorewrite-example} for examples showing the use of
 this tactic. 
 
 % En attente d'un moyen de valoriser les fichiers de demos
@@ -3336,7 +3336,7 @@ e.g. \texttt{Require Import A.}).
   ``\verb#...#''. In this case the tactic command typed by the user is
   equivalent to \tac$_1$;{\tac}.
 
-\SeeAlso {\tt Proof.} in section~\ref{BeginProof}.
+\SeeAlso {\tt Proof.} in Section~\ref{BeginProof}.
 
 \subsubsection[\tt Declare Implicit Tactic {\tac}.]{\tt Declare Implicit Tactic {\tac}.\comindex{Declare Implicit Tactic}}
 
@@ -3480,7 +3480,7 @@ where it was defined. If you want that a
 tactic macro defined in a module is usable in the modules that
 require it, you should put it outside of any section.
 
-The chapter~\ref{TacticLanguage} gives examples of more complex
+Chapter~\ref{TacticLanguage} gives examples of more complex
 user-defined tactics.
 
 
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 951de0cd7..9837c8ba3 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -363,7 +363,7 @@ Qed.
 \end{coq_example*}
 
 \Rem There is a difference between obtaining an induction scheme for a
-function by using \texttt{Function} (section~\ref{Function}) and by
+function by using \texttt{Function} (see Section~\ref{Function}) and by
 using \texttt{Functional Scheme} after a normal definition using
 \texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
 details.
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index 9b3745a0b..d7239c8fd 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -665,7 +665,7 @@ constructor patterns, wild-cards, etc, into terms that only
 use the primitive \textsl{Case} described in Chapter \ref{Cic}
 \item Restoring type coercions and synthesizing the implicit arguments
 (the one denoted by question marks in
-{\Coq} syntax: cf section \ref{Coercions}).
+{\Coq} syntax: see Section~\ref{Coercions}).
 \item Transforming the named bound variables into deBrujin's indexes.
 \item Classifying the global names into the different classes of
 constants (defined constants, constructors, inductive types, etc).
@@ -708,7 +708,7 @@ completed, and a construction can be generated from the proof tree,
 replacing each of the existential variables by its definition.  This
 is exactly what happens when one of the commands
 \texttt{Qed}, \texttt{Save} or \texttt{Defined} is invoked
-(cf. Section \ref{Qed}). The saved theorem becomes a defined constant,
+(see Section~\ref{Qed}). The saved theorem becomes a defined constant,
 whose body is the proof object generated.
 
 \paragraph{Important:} Before being added to the
@@ -766,7 +766,7 @@ arguments for tactics is a union type including:
 \item well-typed terms, represented by a construction;
 \item a substitution for bound variables, like the
 substitution in the tactic \\$\texttt{Apply}\;t\;\texttt{with}\;x:=t_1\ldots
-x_n:=t_n$, (cf. Section~\ref{apply});
+x_n:=t_n$, (see Section~\ref{apply});
 \item a reduction expression, denoting the reduction strategy to be
 followed.
 \end{itemize}
@@ -1013,13 +1013,13 @@ the different kinds of errors used in \Coq{} :
 \fun{val Std.error : string -> 'a}
     {For simple error messages}
 \fun{val Std.errorlabstrm : string -> std\_ppcmds -> 'a}
-    {See section \ref{PrettyPrinter} : this can be used if the user
+    {See Section~\ref{PrettyPrinter} : this can be used if the user
       want to display a term or build a complex error message}
 
 \fun{exception Anomaly of string * std\_ppcmds}
     {This for reporting bugs or things that should not
       happen. The tacticals \texttt{tclTRY} and
-      \texttt{tclTRY} described in section \ref{OcamlTacticals} catch the
+      \texttt{tclTRY} described in Section~\ref{OcamlTacticals} catch the
       exceptions of type \texttt{UserError}, but they don't catch the
       anomalies. So, in your code, don't raise any anomaly, unless you
       know what you are doing. We also recommend to avoid constructs
@@ -1358,7 +1358,7 @@ its associated grammar rules and the commands to generate a module
 that can be loaded dynamically from \Coq's toplevel. 
 
 To compile our project, we will create a \texttt{Makefile} with the
-command \texttt{do\_Makefile} (see section \ref{Makefile}) :
+command \texttt{do\_Makefile} (see Section~\ref{Makefile}) :
 
 \begin{quotation}
   \texttt{do\_Makefile eqdecide.ml EqDecide.v > Makefile}\\
@@ -1489,7 +1489,7 @@ The tactic will depend on the \Coq modules \texttt{Logic} and
 propositional equality (\texttt{eq}), computational disjunction
 (\texttt{sumbool}), and logical negation (\texttt{not}), defined in
 that modules. This is specified creating the module maker
-\texttt{mmk} (cf. Section \ref{Patterns}).
+\texttt{mmk} (see Section~\ref{Patterns}).
 
 The third step of the procedure can be divided into three sub-steps.
 Assume that both $x$ and $y$ have been introduced by the same
@@ -1737,7 +1737,7 @@ is not displayed, since we have chosen to hide its implementation.
 When your tactic does not behave as expected, it is possible to trace
 it dynamically from \Coq. In order to do this, you have first to leave
 the toplevel of \Coq, and come back to the \ocaml{} interpreter. This can
-be done using the command \texttt{Drop} (cf. Section \ref{Drop}). Once
+be done using the command \texttt{Drop} (see Section~\ref{Drop}). Once
 in the \ocaml{} toplevel, load the file \texttt{tactics/include.ml}.
 This file installs several pretty printers for proof trees, goals,
 terms, abstract syntax trees, names, etc.  It also contains the
@@ -1791,7 +1791,7 @@ these macros need to be compiled by giving to {\tt ocamlc} the option
 \verb=-pp "camlp4o -I $(COQTOP)/parsing grammar.cma pa_extend.cmo"=
 
 \noindent which is the default for every file compiled by means of a Makefile
-generated by {\tt coq\_makefile} (cf chapter \ref {Addoc-coqc}). So,
+generated by {\tt coq\_makefile} (see Chapter~\ref{Addoc-coqc}). So,
 just do \verb=make= in this latter case.
 
 The syntax of the macros is given on figure
@@ -1906,7 +1906,7 @@ In case parsing the arguments of the tactic or the vernacular command
 involves grammar entries other than the predefined entries listed
 above, you have to declare a new entry using the macros
 \verb=ARGUMENT EXTEND= or \verb=VERNAC ARGUMENT EXTEND=. The syntax is
-given on figure \ref{ARGUMENT-EXTEND-syntax}. Notice that arguments
+given on Figure~\ref{ARGUMENT-EXTEND-syntax}. Notice that arguments
 declared by \verb=ARGUMENT EXTEND= can be used for arguments of both
 tactics and vernacular commands while arguments declared by
 \verb=VERNAC ARGUMENT EXTEND= can only be used by vernacular commands.
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 8438a6337..2305fa431 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -132,21 +132,21 @@ the sources of \Coq{} somewhere and have an environment variable named
 
 % In the \Coq\ distribution, there is also a separated and independent tool,
 % called {\sf Coq\_SearchIsos}, which allows the search in accordance with {\tt
-% SearchIsos}\index{SearchIsos@{\tt SearchIsos}} (see section~\ref{searchisos})
+% SearchIsos}\index{SearchIsos@{\tt SearchIsos}} (see Section~\ref{searchisos})
 % in a \Coq\ proofs library. More precisely, this program begins, once launched
 % by {\tt coqtop -searchisos}\index{coqtopsearchisos@{\tt
 % coqtop -searchisos}}, loading lightly (by using specifications functions)
 % all the \Coq\ objects files ({\tt .vo}) accessible by the {\tt LoadPath} (see
-% section~\ref{loadpath}). Next, a prompt appears and four commands are then
+% Section~\ref{loadpath}). Next, a prompt appears and four commands are then
 % available:
 
 % \begin{description}
 % \item [{\tt SearchIsos}]\ \\
 %   Scans the fixed context.
 % \item [{\tt Time}]\index{Time@{\tt Time}}\ \\
-%   Turns on the Time Search Display mode (see section~\ref{time}).
+%   Turns on the Time Search Display mode (see Section~\ref{time}).
 % \item [{\tt Untime}]\index{Untime@{\tt Untime}}\ \\
-%   Turns off the Time Search Display mode (see section~\ref{time}).
+%   Turns off the Time Search Display mode (see Section~\ref{time}).
 % \item [{\tt Quit}]\index{Quit@{\tt Quit}}\ \\
 %   Ends the {\tt coqtop -searchisos} session.
 % \end{description}