diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b026397abf..2c2a8fe49e 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -15,7 +15,6 @@ open Names open Constr open Libnames open Globnames -open Nametab open Libobject open Mod_subst @@ -228,14 +227,14 @@ let string_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" | CL_CONST sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_PROJ sp -> let sp = Projection.Repr.constant sp in - string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_IND sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (IndRef sp)) | CL_SECVAR sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (VarRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (VarRef sp)) let pr_class x = str (string_of_class x) @@ -380,7 +379,7 @@ type coercion = { (* Computation of the class arity *) let reference_arity_length ref = - let t, _ = Global.type_of_global_in_context (Global.env ()) ref in + let t, _ = Typeops.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 = @@ -520,7 +519,7 @@ module CoercionPrinting = let compare = GlobRef.Ordered.compare let encode = coercion_of_reference let subst = subst_coe_typ - let printer x = pr_global_env Id.Set.empty x + let printer x = Nametab.pr_global_env Id.Set.empty x let key = ["Printing";"Coercion"] let title = "Explicitly printed coercions: " let member_message x b = |