diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 0926c93e57..20cb43b24e 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -9,6 +9,7 @@ (*i*) open Names open Term +open Constr open Vars open Environ open Nametab @@ -98,7 +99,7 @@ let type_ctx_instance evars env ctx inst subst = let id_of_class cl = match cl.cl_impl with - | ConstRef kn -> let _,_,l = repr_con kn in Label.to_id l + | ConstRef kn -> let _,_,l = Constant.repr3 kn in Label.to_id l | IndRef (kn,i) -> let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in mip.(0).Declarations.mind_typename @@ -179,7 +180,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Name id -> let sp = Lib.make_path id in if Nametab.exists_cci sp then - user_err ~hdr:"new_instance" (Nameops.pr_id id ++ Pp.str " already exists."); + user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists."); id | Anonymous -> let i = Nameops.add_suffix (id_of_class k) "_instance_0" in |