From 9f6eeaee6c1bd67278e7d35e400ede7e7c2ac2fd Mon Sep 17 00:00:00 2001 From: emakarov 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