aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/class.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/class.ml')
-rw-r--r--vernac/class.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/class.ml b/vernac/class.ml
index 3915148a0..061f3efcc 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -173,8 +173,8 @@ let get_strength stre ref cls clt =
let ident_key_of_class = function
| CL_FUN -> "Funclass"
| CL_SORT -> "Sortclass"
- | CL_CONST sp | CL_PROJ sp -> Label.to_string (con_label sp)
- | CL_IND (sp,_) -> Label.to_string (mind_label sp)
+ | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp)
+ | CL_IND (sp,_) -> Label.to_string (MutInd.label sp)
| CL_SECVAR id -> Id.to_string id
(* Identity coercion *)