aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--library/kindops.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/library/kindops.mli b/library/kindops.mli
index 14be70a91..fd7f76dbd 100644
--- a/library/kindops.mli
+++ b/library/kindops.mli
@@ -12,5 +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 :
- locality * definition_object_kind -> string
+val string_of_definition_kind : definition_kind -> string