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, 20 insertions, 20 deletions

diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 64aefee1f6..9063591b64 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -139,13 +139,13 @@ A parametric relation
 can be declared with the following command
 
 \comindex{Add Relation}
-\begin{verse}
+\begin{quote}
   \texttt{Add Relation} \textit{A Aeq}\\
   ~\zeroone{\texttt{reflexivity proved by} \textit{refl}}\\
   ~\zeroone{\texttt{symmetry proved by} \textit{sym}}\\
   ~\zeroone{\texttt{transitivity proved by} \textit{trans}}\\
   \texttt{~as} \textit{id}.
-\end{verse}
+\end{quote}
 after having required the \texttt{Setoid} module with the
 \texttt{Require Setoid} command.
 
@@ -182,14 +182,14 @@ that are syntactic compositions of parametric morphism instances declared with
 the following command.
 
 \comindex{Add Morphism}
-\begin{verse}
+\begin{quote}
   \texttt{Add Morphism} \textit{f}\\
   \texttt{~with signature} \textit{sig}\\
   \texttt{~as id}.\\
   \texttt{Proof}\\
   ~\ldots\\
   \texttt{Qed}
-\end{verse}
+\end{quote}
 
 The command declares \textit{f} as a parametric morphism of signature
 \textit{sig}. The identifier \textit{id} gives a unique name to the morphism
@@ -361,12 +361,12 @@ set of alternative new goals. To force one particular choice, the user
 can switch to the following alternative syntax for rewriting:
 
 \comindex{setoid\_rewrite}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}
   \zeroone{\texttt{in} \textit{ident}}\\
   \texttt{~generate side conditions}
   \textit{term}$_1$ \ldots \textit{term}$_n$\\
-\end{verse}
+\end{quote}
 Up to the \texttt{generate side conditions} part, the syntax is 
 equivalent to the
 one of the \texttt{rewrite} tactic. Additionally, the user can specify a list
@@ -460,41 +460,41 @@ the prefixed tactics it is possible to pass additional arguments such as
 \texttt{generate side conditions} or \texttt{using relation}.
 
 \comindex{setoid\_reflexivity}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_reflexivity}
-\end{verse}
+\end{quote}
 
 \comindex{setoid\_symmetry}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_symmetry}
   \zeroone{\texttt{in} \textit{ident}}\\
-\end{verse}
+\end{quote}
 
 \comindex{setoid\_transitivity}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_transitivity}
-\end{verse}
+\end{quote}
 
 \comindex{setoid\_rewrite}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}\\
   ~\zeroone{\texttt{in} \textit{ident}}\\
   ~\zeroone{\texttt{generate side conditions}
   \textit{term}$_1$ \ldots \textit{term}$_n$}\\
-\end{verse}
+\end{quote}
 
 The \texttt{generate side conditions} argument cannot be passed to the
 unprefixed form.
 
 \comindex{setoid\_replace}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_replace} \textit{term} \texttt{with} \textit{term}
   ~\zeroone{\texttt{in} \textit{ident}}\\
   ~\zeroone{\texttt{using relation} \textit{term}}\\
   ~\zeroone{\texttt{generate side conditions}
   \textit{term}$_1$ \ldots \textit{term}$_n$}\\
   ~\zeroone{\texttt{by} \textit{tactic}}
-\end{verse}
+\end{quote}
 
 The  \texttt{generate  side  conditions} and  \texttt{using  relation}
 arguments cannot be passed to the unprefixed form. The latter argument
@@ -521,9 +521,9 @@ Due to backward compatibility reasons, the following syntax for the
 declaration of setoids and morphisms is also accepted.
 
 \comindex{Add Setoid}
-\begin{verse}
+\begin{quote}
   \texttt{Add Setoid} \textit{A Aeq ST} \texttt{as} \textit{ident}
-\end{verse}
+\end{quote}
 where \textit{Aeq} is a congruence relation without parameters,
 \textit{A} is its carrier and \textit{ST} is an object of type
 \verb|(Setoid_Theory A Aeq)| (i.e. a record packing together the reflexivity,
@@ -531,12 +531,12 @@ symmetry and transitivity lemmas). Notice that the syntax is not completely
 backward compatible since the identifier was not required.
 
 \comindex{Add Morphism}
-\begin{verse}
+\begin{quote}
   \texttt{Add Morphism} \textit{ f }:\textit{ ident}.\\
   Proof.\\
   \ldots\\
   Qed.
-\end{verse}
+\end{quote}
 
 The latter command is restricted to the declaration of morphisms without
 parameters. It is not fully backward compatible since the property the user