aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/output.mli
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-18 16:02:49 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-18 16:02:49 +0000
commitf90854e62a8025eb1477c743dfef64a66f7da535 (patch)
tree4f3fb3a742e69c5c0212bb58cc18cb1ff609bc29 /tools/coqdoc/output.mli
parent2da5db43c3937b7a74107d5a1e4e23a58ac6af28 (diff)
Various minor fixes to coqdoc from A. Chlipala.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15624 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/output.mli')
-rw-r--r--tools/coqdoc/output.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 53d886668..b68857b27 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -60,6 +60,7 @@ val rule : unit -> unit
val nbsp : unit -> unit
val char : char -> unit
+val keyword : string -> loc -> unit
val ident : string -> loc -> unit
val sublexer : char -> loc -> unit
val initialize : unit -> unit