diff options
Diffstat (limited to 'doc/refman/Reference-Manual.tex')
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 134641596..34399196b 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -1,9 +1,9 @@ -\RequirePackage{ifpdf} -\ifpdf - \documentclass[11pt,a4paper,pdftex]{book} -\else +%\RequirePackage{ifpdf} +%\ifpdf +% \documentclass[11pt,a4paper,pdftex]{book} +%\else \documentclass[11pt,a4paper]{book} -\fi +%\fi \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} @@ -14,8 +14,8 @@ \usepackage{amssymb} \usepackage{alltt} \usepackage{hevea} - \usepackage{ifpdf} +\usepackage{headers} % in this directory % for coqide \ifpdf % si on est pas en pdflatex @@ -25,12 +25,11 @@ \fi -%\includeonly{RefMan-gal.v,RefMan-ltac.v,RefMan-lib.v,Cases.v} +%\includeonly{Setoid} \input{../common/version.tex} \input{../common/macros.tex}% extension .tex pour htmlgen \input{../common/title.tex}% extension .tex pour htmlgen -\input{./headers.tex}% extension .tex pour htmlgen \begin{document} %BEGIN LATEX @@ -56,7 +55,9 @@ %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 |