typographie

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

1 files changed, 24 insertions, 24 deletions

diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex
index ee4be7560..9bcf2de77 100755
--- a/doc/RefMan-int.tex
+++ b/doc/RefMan-int.tex
@@ -58,37 +58,37 @@ below.
 
 \begin{itemize}
 \item The first part describes the specification language,
-  Gallina. The chapters \ref{Gallina} and \ref{Gallina-extension}
+  Gallina. Chapters~\ref{Gallina} and~\ref{Gallina-extension}
   describe the concrete syntax as well as the meaning of programs,
-  theorems and proofs in the Calculus of Inductive Constructions. The
-  chapter \ref{Theories} describes the standard library of \Coq. The
-  chapter \ref{Cic} is a mathematical description of the
-  formalism. The chapter \ref{Modules} describes the module system.
+  theorems and proofs in the Calculus of Inductive
+  Constructions. Chapter~\ref{Theories} describes the standard library
+  of \Coq. Chapter~\ref{Cic} is a mathematical description of the
+  formalism. Chapter~\ref{Modules} describes the module system.
 
 \item The second part describes the proof engine. It is divided in
-  for chapters. Chapter \ref{Vernacular-commands} presents
-  all commands (we call them \textit{vernacular commands}) that are not
+  four chapters. Chapter~\ref{Vernacular-commands} presents
+  all commands (we call them \emph{vernacular commands}) that are not
   directly related to interactive proving: requests to the environment,
   complete or partial evaluation, loading and compiling files. How to
   start and stop proofs, do multiple proofs in parallel is explained
-  in the chapter \ref{Proof-handling}. In chapter \ref{Tactics}, 
+  in Chapter~\ref{Proof-handling}. In Chapter~\ref{Tactics}, 
   all commands that realize one or more steps of the proof are
-  presented: we call them  \textit{tactics}. Examples of tactics are
-  described in chapter~\ref{Tactics-examples}.
+  presented: we call them  \emph{tactics}. Examples of tactics are
+  described in Chapter~\ref{Tactics-examples}.
 
 \item The third part describes how to extend the system in two ways:
-  adding parsing and pretty-printing rules (chapter
-  \ref{Addoc-syntax}) and writing new tactics (chapter
-  \ref{TacticLanguage})
+  adding parsing and pretty-printing rules
+  (Chapter~\ref{Addoc-syntax}) and writing new tactics
+  (Chapter~\ref{TacticLanguage}). 
 
 
 \item In the fourth part more practical tools are documented. First in
-  the chapter \ref{Addoc-coqc} the usage of \texttt{coqc} (batch mode)
+  Chapter~\ref{Addoc-coqc}, the usage of \texttt{coqc} (batch mode)
   and \texttt{coqtop} (interactive mode) with their options is
-  described. Then (in chapter \ref{Utilities}) 
+  described. Then, in Chapter~\ref{Utilities},
   various utilities that come with the \Coq\ distribution are
   presented.
-  Finally, chapter~\ref{Addoc-coqide} describes the \Coq{} integrated
+  Finally, Chapter~\ref{Addoc-coqide} describes the \Coq{} integrated
   development environment. 
 \end{itemize}
 
@@ -97,14 +97,14 @@ a tactic index and a vernacular command index.
 
 \section*{List of additional documentation}
 
-This manual contains not all the documentation the user may need about
-Coq. Various informations can be found in the following documents: 
-
+This manual does not contain all the documentation the user may need
+about \Coq{}. Various informations can be found in the following
+documents:  
 \begin{description}
 
 \item[Tutorial] 
-  A companion volume to this reference manual, the \Coq\ Tutorial, is
-  aimed at gently introducing new users to developing proofs in \Coq\
+  A companion volume to this reference manual, the \Coq{} Tutorial, is
+  aimed at gently introducing new users to developing proofs in \Coq{}
   without assuming prior knowledge of type theory. In a second step, the
   user can read also the tutorial on recursive types (document {\tt
     RecTutorial.ps}).
@@ -119,11 +119,11 @@ Coq. Various informations can be found in the following documents:
   to the Addendum. 
 
 \item[Installation] A text file INSTALL that comes with the sources
-  explains how to install \Coq. A file UNINSTALL explains how
+  explains how to install \Coq{}. A file UNINSTALL explains how
   uninstall or move it.
 
-\item[The \Coq\ standard library]
-A commented version of sources of the \Coq\ standard library
+\item[The \Coq{} standard library]
+A commented version of sources of the \Coq{} standard library
 (including only the specifications, the proofs are removed) 
 is given in the additional document {\tt Library.ps}.