aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/output.ml
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-02-27 13:18:33 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-02-27 13:18:33 +0000
commit5b89cbf55612395effaebc5f17be266dc25fe008 (patch)
treef3cf9d8deec1bff92fdb0636c5487e3c1cd60174 /tools/coqdoc/output.ml
parent34315746efd0d9405999b6db21e19b8cc71e3471 (diff)
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5389 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/output.ml')
-rw-r--r--tools/coqdoc/output.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index ebcb16c04..43f962330 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -141,7 +141,10 @@ let _ = List.iter
"~", "\\ensuremath{\\lnot}";
"/\\", "\\ensuremath{\\land}";
"\\/", "\\ensuremath{\\lor}";
- "|-", "\\ensuremath{\\vdash}" ]
+ "|-", "\\ensuremath{\\vdash}";
+ "forall", "\\ensuremath{\\forall}";
+ "exists", "\\ensuremath{\\exists}";
+ ]
(*s Table of contents *)