From 9f6eeaee6c1bd67278e7d35e400ede7e7c2ac2fd Mon Sep 17 00:00:00 2001
From: emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 10 Apr 2007 14:02:16 +0000
Subject: 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
---
 doc/refman/AddRefMan-pre.tex | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc/refman/AddRefMan-pre.tex')

diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
index 5312b8fc2..15776690c 100644
--- a/doc/refman/AddRefMan-pre.tex
+++ b/doc/refman/AddRefMan-pre.tex
@@ -1,6 +1,8 @@
 %\coverpage{Addendum to the Reference Manual}{\ }
 %\addcontentsline{toc}{part}{Additional documentation}
+%BEGIN LATEX
 \setheaders{Presentation of the Addendum}
+%END LATEX
 \chapter*{Presentation of the Addendum}
 
 Here you will find several pieces of additional documentation for the
-- 
cgit v1.2.3

