aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/kindops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/kindops.mli')
-rw-r--r--library/kindops.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/kindops.mli b/library/kindops.mli
index 77979c915..06f873e85 100644
--- a/library/kindops.mli
+++ b/library/kindops.mli
@@ -12,4 +12,4 @@ open Decl_kinds
val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
val string_of_theorem_kind : theorem_kind -> string
-val string_of_definition_kind : definition_kind -> string
+val string_of_definition_object_kind : definition_object_kind -> string