summaryrefslogtreecommitdiff
path: root/doc/refman/Reference-Manual.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/Reference-Manual.tex')
-rw-r--r--doc/refman/Reference-Manual.tex151
1 files changed, 0 insertions, 151 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
deleted file mode 100644
index b0ada528..00000000
--- a/doc/refman/Reference-Manual.tex
+++ /dev/null
@@ -1,151 +0,0 @@
-%\RequirePackage{ifpdf}
-%\ifpdf
-% \documentclass[11pt,a4paper,pdftex]{book}
-%\else
- \documentclass[11pt,a4paper]{book}
-%\fi
-
-\usepackage[latin1]{inputenc}
-\usepackage[T1]{fontenc}
-\usepackage{times}
-\usepackage{url}
-\usepackage{verbatim}
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{alltt}
-\usepackage{hevea}
-\usepackage{ifpdf}
-\usepackage[headings]{fullpage}
-\usepackage{headers} % in this directory
-\usepackage{multicol}
-\usepackage{xspace}
-
-% for coqide
-\ifpdf % si on est pas en pdflatex
- \usepackage[pdftex]{graphicx}
-\else
- \usepackage[dvips]{graphicx}
-\fi
-
-
-%\includeonly{Setoid}
-
-\input{../common/version.tex}
-\input{../common/macros.tex}% extension .tex pour htmlgen
-\input{../common/title.tex}% extension .tex pour htmlgen
-%\input{headers}
-
-\usepackage[linktocpage,colorlinks,bookmarks=false]{hyperref}
-% The manual advises to load hyperref package last to be able to redefine
-% necessary commands.
-% The above should work for both latex and pdflatex. Even if PDF is produced
-% through DVI and PS using dvips and ps2pdf, hyperlinks should still work.
-% linktocpage option makes page numbers, not section names, to be links in
-% the table of contents.
-% colorlinks option colors the links instead of using boxes.
-
-% The command \tocnumber was added to HEVEA in version 1.06-6.
-% It instructs HEVEA to put chapter numbers into the table of
-% content entries. The table of content is produced by HACHA using
-% the options -tocbis -o toc.html. HEVEA produces a warning when
-% a command is not recognized, so versions earlier than 1.06-6 can
-% still be used.
-%HEVEA\tocnumber
-
-\begin{document}
-%BEGIN LATEX
-\sloppy\hbadness=5000
-%END LATEX
-
-%BEGIN LATEX
-\coverpage{Reference Manual}
-{The Coq Development Team}
-{This material may be distributed only subject to the terms and
-conditions set forth in the Open Publication License, v1.0 or later
-(the latest version is presently available at
-\url{http://www.opencontent.org/openpub}).
-Options A and B of the licence are {\em not} elected.}
-%END LATEX
-
-%\defaultheaders
-\include{RefMan-int}% Introduction
-\include{RefMan-pre}% Credits
-
-%BEGIN LATEX
-\tableofcontents
-%END LATEX
-
-\part{The language}
-%BEGIN LATEX
-\defaultheaders
-%END LATEX
-\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.v}% Writing tactics
-\include{RefMan-tacex.v}% Detailed Examples of tactics
-\include{RefMan-decl.v}% The mathematical proof language
-
-\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}%
-\include{Classes.v}%
-%%SUPPRIME \include{Natural.v}%
-\include{Omega.v}%
-\include{Micromega.v}
-%%SUPPRIME \include{Correctness.v}% = preuve de pgms imperatifs
-\include{Extraction.v}%
-\include{Program.v}%
-\include{Polynom.v}% = Ring
-\include{Nsatz.v}%
-\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
-
-\end{document}
-
-
-% $Id: Reference-Manual.tex 14090 2011-05-03 13:34:16Z pboutill $