[Sphinx] Add introduction

I backported changes done to the LaTeX manual.

1 files changed, 108 insertions, 132 deletions

diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index f802a3595..514745c1b 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -1,143 +1,119 @@
-%BEGIN LATEX
-\setheaders{Introduction}
-%END LATEX
-\chapter*{Introduction}
-%HEVEA\cutname{introduction.html}
-
-This document is the Reference Manual of version \coqversion{} of the \Coq\ 
-proof assistant. A companion volume, the \Coq\ Tutorial, is provided
-for the beginners. It is advised to read the Tutorial first.
-A book~\cite{CoqArt} on practical uses of the \Coq{} system was published in 2004 and is a good support for both the beginner and
-the advanced user.
-
-%The system \Coq\ is designed to develop mathematical proofs. It can be
-%used by mathematicians to develop mathematical theories and by
-%computer scientists to write formal specifications,
-The \Coq{} system is designed to develop mathematical proofs, and
+------------------------
+Introduction
+------------------------
+
+This document is the Reference Manual of version of the |Coq|  proof
+assistant. A companion volume, the |Coq| Tutorial, is provided for the
+beginners. It is advised to read the Tutorial first. A
+book :cite:`CoqArt` on practical uses of the |Coq| system was
+published in 2004 and is a good support for both the beginner and the
+advanced user.
+
+The |Coq| system is designed to develop mathematical proofs, and
 especially to write formal specifications, programs and to verify that
-programs are correct with respect to their specification. It provides
-a specification language named \gallina. Terms of \gallina\ can
-represent programs as well as properties of these programs and proofs
-of these properties. Using the so-called \textit{Curry-Howard
-  isomorphism}, programs, properties and proofs are formalized in the
-same language called \textit{Calculus of Inductive Constructions},
-that is a $\lambda$-calculus with a rich type system.  All logical
-judgments in \Coq\ are typing judgments. The very heart of the Coq
-system is the type-checking algorithm that checks the correctness of
-proofs, in other words that checks that a program complies to its
-specification. \Coq\ also provides an interactive proof assistant to
-build proofs using specific programs called \textit{tactics}.
-
-All services of the \Coq\ proof assistant are accessible by
-interpretation of a command language called \textit{the vernacular}.
-
-\Coq\ has an interactive mode in which commands are interpreted as the
-user types them in from the keyboard and a compiled mode where
-commands are processed from a file.  
-
-\begin{itemize}
-\item The interactive mode may be used as a debugging mode in which
-  the user can develop his theories and proofs step by step,
-  backtracking if needed and so on. The interactive mode is run with
-  the {\tt coqtop} command from the operating system (which we shall
-  assume to be some variety of UNIX in the rest of this document).
-\item The compiled mode acts as a proof checker taking a file
-  containing a whole development in order to ensure its correctness.
-  Moreover, \Coq's compiler provides an output file containing a
-  compact representation of its input. The compiled mode is run with
-  the {\tt coqc} command from the operating system. 
-
-\end{itemize}
-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
-({\ProofGeneral}~\cite{ProofGeneral}) or through a customized interface
-(PCoq~\cite{Pcoq}).  These facilities are not documented here.  There
-is also a \Coq{} Integrated Development Environment described in
-Chapter~\ref{Addoc-coqide}.
-
-\section*{How to read this book}
+programs are correct with respect to their specification. It provides a
+specification language named |Gallina|. Terms of |Gallina| can represent
+programs as well as properties of these programs and proofs of these
+properties. Using the so-called *Curry-Howard isomorphism*, programs,
+properties and proofs are formalized in the same language called
+*Calculus of Inductive Constructions*, that is a
+:math:`\lambda`-calculus with a rich type system. All logical judgments
+in |Coq| are typing judgments. The very heart of the |Coq| system is the
+type-checking algorithm that checks the correctness of proofs, in other
+words that checks that a program complies to its specification. |Coq| also
+provides an interactive proof assistant to build proofs using specific
+programs called *tactics*.
+
+All services of the |Coq| proof assistant are accessible by interpretation
+of a command language called *the vernacular*.
+
+Coq has an interactive mode in which commands are interpreted as the
+user types them in from the keyboard and a compiled mode where commands
+are processed from a file.
+
+-  The interactive mode may be used as a debugging mode in which the
+   user can develop his theories and proofs step by step, backtracking
+   if needed and so on. The interactive mode is run with the `coqtop` 
+   command from the operating system (which we shall assume to be some
+   variety of UNIX in the rest of this document).
+
+-  The compiled mode acts as a proof checker taking a file containing a
+   whole development in order to ensure its correctness. Moreover,
+   |Coq|’s compiler provides an output file containing a compact
+   representation of its input. The compiled mode is run with the `coqc`
+   command from the operating system.
+
+These two modes are documented in Chapter :ref:`thecoqcommands`.
+
+Other modes of interaction with |Coq| are possible: through an emacs shell
+window, an emacs generic user-interface for proof assistant (Proof
+General :cite:`ProofGeneral`) or through a customized
+interface (PCoq :cite:`Pcoq`). These facilities are not
+documented here. There is also a |Coq| Integrated Development Environment
+described in :ref:`coqintegrateddevelopmentenvironment`.
+
+How to read this book
+=====================
 
 This is a Reference Manual, not a User Manual, so it is not made for a
 continuous reading. However, it has some structure that is explained
 below.
 
-\begin{itemize}
-\item The first part describes the specification language,
-  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. Chapter~\ref{Theories} describes the standard library
-  of \Coq. Chapter~\ref{Cic} is a mathematical description of the
-  formalism. Chapter~\ref{chapter:Modules} describes the module system.
-
-\item The second part describes the proof engine. It is divided in
-  five 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 Chapter~\ref{Proof-handling}. In
-  Chapter~\ref{Tactics}, all commands that realize one or more steps
-  of the proof are presented: we call them \emph{tactics}. The
-  language to combine these tactics into complex proof strategies is
-  given in Chapter~\ref{TacticLanguage}. 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}). 
-
-\item The third part describes how to extend the syntax of \Coq. It
-corresponds to the Chapter~\ref{Addoc-syntax}.
-
-\item In the fourth part more practical tools are documented. First in
-  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},
-  various utilities that come with the \Coq\ distribution are
-  presented.
-  Finally, Chapter~\ref{Addoc-coqide} describes the \Coq{} integrated
-  development environment. 
-
-\item The fifth part documents a number of advanced features, including
-  coercions, canonical structures, typeclasses, program extraction, and
-  specialized solvers and tactics.  See the table of contents for a complete
-  list.
-\end{itemize}
+-  The first part describes the specification language, |Gallina|.
+   Chapters :ref:`thegallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete
+   syntax as well as the meaning of programs, theorems and proofs in the
+   Calculus of Inductive Constructions. Chapter :ref:`thecoqlibrary` describes the
+   standard library of |Coq|. Chapter :ref:`calculusofinductiveconstructions` is a mathematical description
+   of the formalism. Chapter :ref:`themodulesystem` describes the module
+   system.
+
+-  The second part describes the proof engine. It is divided in five
+   chapters. Chapter :ref:`vernacularcommands` presents all commands (we
+   call them *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
+   Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that
+   realize one or more steps of the proof are presented: we call them
+   *tactics*. The language to combine these tactics into complex proof
+   strategies is given in Chapter :ref:`thetacticlanguage`. Examples of tactics
+   are described in Chapter :ref:`detailedexamplesoftactics`.
+
+-  The third part describes how to extend the syntax of |Coq|. It
+   corresponds to the Chapter :ref:`syntaxextensionsandinterpretationscopes`.
+
+-  In the fourth part more practical tools are documented. First in
+   Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and
+   `coqtop` (interactive mode) with their options is described. Then,
+   in Chapter :ref:`utilities`, various utilities that come with the
+   |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` 
+   describes the |Coq| integrated development environment.
+
+-  The fifth part documents a number of advanced features, including coercions,
+   canonical structures, typeclasses, program extraction, and specialized
+   solvers and tactics. See the table of contents for a complete list.
 
 At the end of the document, after the global index, the user can find
-specific indexes for tactics, vernacular commands, and error
-messages. 
+specific indexes for tactics, vernacular commands, and error messages.
 
-\section*{List of additional documentation}
+List of additional documentation
+================================
 
 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{}
-  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}).
-
-\item[Installation] A text file INSTALL that comes with the sources
-  explains how to install \Coq{}.
-
-\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}.
-
-\end{description}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End:
+about |Coq|. Various informations can be found in the following documents:
+
+Tutorial
+    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
+    `RecTutorial.ps`).
+
+Installation
+    A text file `INSTALL` that comes with the sources explains how to
+    install |Coq|.
+
+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 `Library.ps`.