aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/coqdoc.sty
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/coqdoc.sty')
-rw-r--r--tools/coqdoc/coqdoc.sty3
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index ef4f41195..fca9a1d76 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -70,6 +70,9 @@
% !!! CAUTION: This environment may have empty contents
\newenvironment{coqdoccode}{}{}
+% Environment for comments
+\newenvironment{coqdoccomment}{\tt(*}{*)}
+
% newline and indentation
%BEGIN LATEX
% Base indentation length