aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/coqdoc.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/coqdoc.tex')
-rw-r--r--doc/refman/coqdoc.tex6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index f2630da07..48e91fcd2 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -6,9 +6,9 @@
\newcommand{\texmacs}{\TeX{}macs}
\newcommand{\monurl}[1]{#1}
%HEVEA\renewcommand{\monurl}[1]{\ahref{#1}{#1}}
-%HEVEA\newcommand{\lnot}{not}
-%HEVEA\newcommand{\lor}{or}
-%HEVEA\newcommand{\land}{\&}
+%\newcommand{\lnot}{not} % Hevea handles these symbols nicely
+%\newcommand{\lor}{or}
+%\newcommand{\land}{\&}
%%% attention : -- dans un argument de \texttt est affiché comme un
%%% seul - d'où l'utilisation de la macro suivante
\newcommand{\mm}{\symbol{45}\symbol{45}}