%\RequirePackage{ifpdf}
%\ifpdf
%  \documentclass[11pt,a4paper,pdftex]{book}
%\else
  \documentclass[11pt,a4paper]{book}
%\fi

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{textcomp}
\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}
\usepackage{pmboxdraw}
\usepackage{float}
\usepackage{color}
  \definecolor{dkblue}{rgb}{0,0.1,0.5}
  \definecolor{lightblue}{rgb}{0,0.5,0.5}
  \definecolor{dkgreen}{rgb}{0,0.4,0}
  \definecolor{dk2green}{rgb}{0.4,0,0}
  \definecolor{dkviolet}{rgb}{0.6,0,0.8}
  \definecolor{dkpink}{rgb}{0.2,0,0.6}
\usepackage{listings}
  \def\lstlanguagefiles{coq-listing.tex}
\usepackage{tabularx}
\usepackage{array,longtable}

\floatstyle{boxed} 
\restylefloat{figure}

% 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=true,bookmarksnumbered=true]{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.v}% Proof handling
\include{RefMan-tac.v}% Tactics and tacticals
\include{RefMan-ltac.v}% Writing tactics
\include{RefMan-tacex.v}% Detailed Examples of tactics

\lstset{language=SSR}
\lstset{moredelim=[is][]{|*}{*|}}
\lstset{moredelim=*[is][\itshape\rmfamily]{/*}{*/}}
\include{RefMan-ssr}

\part{User extensions}
\include{RefMan-syn.v}% The Syntax and the Grammar commands
%%SUPPRIME \include{RefMan-tus.v}% Writing tactics
\include{RefMan-sch.v}% The Scheme commands

\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{CanonicalStructures.v}%
\include{Classes.v}%
\include{Omega.v}%
\include{Micromega.v}
\include{Extraction.v}%
\include{Program.v}%
\include{Polynom.v}%  = Ring
\include{Nsatz.v}%
\include{Setoid.v}% Tactique pour les setoides
\include{AsyncProofs}% Paral-ITP
\include{Universes.v}% Universe polymorphes
\include{Misc.v}
%BEGIN LATEX
\RefManCutCommand{ENDADDENDUM=\thepage}
%END LATEX
\nocite{*}
\bibliographystyle{plain}
\bibliography{biblio}
\cutname{biblio.html}

\printrefmanindex{default}{Global Index}{general-index.html}
\printrefmanindex{tactic}{Tactics Index}{tactic-index.html}
\printrefmanindex{command}{Vernacular Commands Index}{command-index.html}
\printrefmanindex{option}{Vernacular Options Index}{option-index.html}
\printrefmanindex{error}{Index of Error Messages}{error-index.html}

%BEGIN LATEX
\cleardoublepage
\phantomsection
\addcontentsline{toc}{chapter}{\listfigurename}
\listoffigures
%END LATEX

\end{document}