aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/output.ml
diff options
context:
space:
mode:
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 *)