aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2016-10-27 10:57:02 +0200
committerGravatar Matej Kosik <matej.kosik@inria.fr>2016-10-27 10:57:02 +0200
commitebc07e5741fab0df15a8de56fc69397a7d164ce9 (patch)
treecea27a714491d073af1224e0daf6f04dc9f471a8 /intf
parenta9dcb4dc1c9ec4fd8bf22450402f443ec15d8f09 (diff)
COMMENT: unfortunatelly, ocamldoc does not recognize this kind of markup: it generates garbage. So the comment is kept but it is not passed over to ocamldoc.
Diffstat (limited to 'intf')
-rw-r--r--intf/decl_kinds.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
index 6a4e18833..8254b1b80 100644
--- a/intf/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -41,7 +41,7 @@ type definition_object_kind =
type assumption_object_kind = Definitional | Logical | Conjectural
-(** [assumption_kind]
+(* [assumption_kind]
| Local | Global
------------------------------------