Eliminated warning messages from Hevea. Most warning messages were

from commands about headers; where appropriate, surrounded those by
%BEGIN LATEX ... %END LATEX. Removed some \newcommands that were
ignored. Removed redefinitions of \land, \lor, \lnot: there are nicely
handled by Hevea.

Split headers.tex file into headers.sty (for LaTeX) and headers.hva
(for Hevea). This allowed removing comments like %BEGIN LATEX and %HEVEA
and also commands \makeatletter, \makeatother.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9752 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 8 deletions

diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 1346415968..34399196be 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