aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-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 8d5c2fb687..8decdbea1e 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -46,7 +46,7 @@ type definition_object_kind =
| Method
| Let
-type assumption_object_kind = Definitional | Logical | Conjectural
+type assumption_object_kind = Definitional | Logical | Conjectural | Context
(* [assumption_kind]