aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/decl_kinds.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index c6879575d..c33738644 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -24,6 +24,7 @@ type theorem_kind =
| Fact
| Remark
| Property
+ | Proposition
| Corollary
type definition_object_kind =
@@ -80,8 +81,9 @@ let string_of_theorem_kind = function
| Lemma -> "Lemma"
| Fact -> "Fact"
| Remark -> "Remark"
- | Corollary -> "Corollary"
| Property -> "Property"
+ | Proposition -> "Proposition"
+ | Corollary -> "Corollary"
let string_of_definition_kind (l,boxed,d) =
match (l,d) with