[Sphinx] Move introduction to new infrastructure

2 files changed, 0 insertions, 144 deletions

diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex
deleted file mode 100644
index f802a35950..0000000000
--- a/doc/refman/RefMan-int.tex
+++ /dev/null
@@ -1,143 +0,0 @@
-%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
-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}
-
-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}
-
-At the end of the document, after the global index, the user can find
-specific indexes for tactics, vernacular commands, and error
-messages. 
-
-\section*{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:
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index fc1c01cf24..1bd79d5112 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -85,7 +85,6 @@ Options A and B of the licence are {\em not} elected.}
 %END LATEX
 
 %\defaultheaders
-\include{RefMan-int}% Introduction
 \include{RefMan-pre}% Credits
 
 %BEGIN LATEX