aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/classops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.ml')
-rw-r--r--pretyping/classops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 948aa26ca..078990a8c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -403,7 +403,7 @@ type coercion = {
(* Computation of the class arity *)
let reference_arity_length ref =
- let t = Universes.unsafe_type_of_global ref in
+ let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
let projection_arity_length p =