1 files changed, 124 insertions, 0 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
new file mode 100644
index 000000000..fa909b607
--- /dev/null
+++ b/doc/refman/Reference-Manual.tex
@@ -0,0 +1,124 @@
+\ifx\pdfoutput\undefined   % si on est pas en pdflatex
+\documentclass[11pt,a4paper]{book}
+\else
+\documentclass[11pt,a4paper,pdftex]{book}
+\fi
+\usepackage[latin1]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{times}
+\usepackage{url}
+\usepackage{verbatim}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{alltt}
+\usepackage{hevea}
+
+% for coqide
+\ifx\pdfoutput\undefined   % si on est pas en pdflatex
+  \usepackage[dvips]{graphicx}
+\else
+  \usepackage[pdftex]{graphicx}
+\fi
+
+
+%\includeonly{RefMan-gal.v,RefMan-ltac.v,RefMan-lib.v,Cases.v}
+
+\input{./version.tex}
+\input{./macros.tex}% extension .tex pour htmlgen
+\input{./title.tex}% extension .tex pour htmlgen
+\input{./headers.tex}% extension .tex pour htmlgen
+
+\begin{document}
+%BEGIN LATEX
+\sloppy\hbadness=5000
+%END LATEX
+
+\tophtml{}
+%BEGIN LATEX
+\coverpage{Reference Manual}{The Coq Development Team}
+%END LATEX
+
+%\defaultheaders
+\include{RefMan-int}% Introduction
+\include{RefMan-pre}% Credits
+
+%BEGIN LATEX
+\tableofcontents
+%END LATEX
+
+\part{The language}
+\defaultheaders
+\include{RefMan-gal.v}% Gallina
+\include{RefMan-ext.v}% Gallina extensions
+\include{RefMan-lib.v}% The coq library
+\include{RefMan-cic.v}% The Calculus of Constructions
+\include{RefMan-modr}% The module system
+
+
+\part{The proof engine}
+\include{RefMan-oth.v}% Vernacular commands
+\include{RefMan-pro}% Proof handling
+\include{RefMan-tac.v}% Tactics and tacticals
+\include{RefMan-ltac}% Writing tactics
+\include{RefMan-tacex.v}% Detailed Examples of tactics
+
+\part{User extensions}
+\include{RefMan-syn.v}% The Syntax and the Grammad commands
+%%SUPPRIME \include{RefMan-tus.v}% Writing tactics
+
+\part{Practical tools}
+\include{RefMan-com}% The coq commands (coqc coqtop)
+\include{RefMan-uti}% utilities (gallina, do_Makefile, etc)
+\include{RefMan-ide}% Coq IDE
+
+%BEGIN LATEX
+\RefManCutCommand{BEGINADDENDUM=\thepage}
+%END LATEX
+\part{Addendum to the Reference Manual}
+\include{AddRefMan-pre}%
+\include{Cases.v}%
+\include{Coercion.v}%
+%%SUPPRIME \include{Natural.v}%
+\include{Omega.v}%
+%%SUPPRIME \include{Program.v}%
+%%SUPPRIME \include{Correctness.v}% = preuve de pgms imperatifs
+\include{Extraction.v}%
+\include{Polynom.v}%  = Ring
+\include{Setoid.v}% Tactique pour les setoides
+%BEGIN LATEX
+\RefManCutCommand{ENDADDENDUM=\thepage}
+%END LATEX
+\nocite{*}
+\bibliographystyle{plain}
+\bibliography{biblio}
+\cutname{biblio.html}
+
+\printindex
+\cutname{general-index.html}
+
+\printindex[tactic]
+\cutname{tactic-index.html}
+
+\printindex[command]
+\cutname{command-index.html}
+
+\printindex[error]
+\cutname{error-index.html}
+
+%BEGIN LATEX
+\listoffigures
+\addcontentsline{toc}{chapter}{\listfigurename}
+%END LATEX
+
+%BEGIN LATEX
+\RefManCutCommand{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps}
+\RefManCutCommand{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps}
+\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-}
+\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM}
+\RefManCutClose
+%END LATEX
+
+\end{document}
+
+
+% $Id$