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 0e2ef95739..4b20016ab2 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -67,7 +67,7 @@ type goal_object_kind =
| DefinitionBody of definition_object_kind
| Proof of theorem_kind
-type goal_kind = locality * polymorphic * goal_object_kind
+type goal_kind = locality * goal_object_kind
(** Kinds used in library *)