aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/decl_kinds.ml
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-10-20 13:50:08 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-10-20 13:50:08 +0000
commit9c6487ba87f448daa28158c6e916e3d932c50645 (patch)
tree31bc965d5d14b34d4ab501cbd2350d1de44750c5 /library/decl_kinds.ml
parent1457d6a431755627e3b52eaf74ddd09c641a9fe3 (diff)
COMMITED BYTECODE COMPILER
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/decl_kinds.ml')
-rw-r--r--library/decl_kinds.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 66b1bb072..597431840 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -23,7 +23,7 @@ type theorem_kind =
| Remark
type definition_object_kind =
- | Definition
+ | Definition of bool
| Coercion
| SubClass
| CanonicalStructure