diff options
Diffstat (limited to 'doc/refman/Reference-Manual.tex')
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 151 |
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 $ |