aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/kindops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/kindops.ml')
-rw-r--r--library/kindops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/kindops.ml b/library/kindops.ml
index 3d737e5ac..21b1bec33 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -24,9 +24,9 @@ let string_of_theorem_kind = function
| Corollary -> "Corollary"
let string_of_definition_kind def =
- let locality = def.locality in
+ let (locality, poly, kind) = def in
let error () = CErrors.anomaly (Pp.str "Internal definition kind") in
- match def.object_kind with
+ match kind with
| Definition ->
begin match locality with
| Discharge -> "Let"