Remove remnants of polymorphic instance name registration.

6 files changed, 3 insertions, 13 deletions

diff --git a/engine/univNames.ml b/engine/univNames.ml
index 5c87fed31c..b7ccd2372f 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -53,8 +53,6 @@ let compute_instance_binders inst ubinders =
   in
   Array.map_to_list map (Instance.to_array inst)
 
-let register_universe_binders ref ubinders = ()
-
 type univ_name_list = Names.lname list
 
 let universe_binders_with_opt_names ref names =
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 634db9581c..b00c5fda95 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -21,8 +21,6 @@ val empty_binders : universe_binders
 
 val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t list
 
-val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
-
 type univ_name_list = Names.lname list
 
 (** [universe_binders_with_opt_names ref l]
diff --git a/interp/declare.ml b/interp/declare.ml
index 29e777d0c6..fe8fc7c969 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -520,7 +520,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
 
 let declare_univ_binders gr pl =
   if Global.is_polymorphic gr then
-    UnivNames.register_universe_binders gr pl
+    ()
   else
     let l = match gr with
       | ConstRef c -> Label.to_id @@ Constant.label c
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3d3d825bd0..d533db7ed9 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -204,7 +204,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
         (** FIXME: include locality *)
         let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
         let gr = ConstRef c in
-        let () = UnivNames.register_universe_binders gr (Evd.universe_binders sigma) in
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
           Impargs.declare_manual_implicits false gr [impls]
       in
diff --git a/vernac/record.ml b/vernac/record.ml
index fb3ef5c09a..ac84003266 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -277,7 +277,7 @@ let warn_non_primitive_record =
                     strbrk" could not be defined as a primitive record")))
 
 (* We build projections *)
-let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields =
+let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
@@ -324,7 +324,6 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
                 (** Already defined by declare_mind silently *)
                 let kn = Projection.Repr.constant p in
                 Declare.definition_message fid;
-                UnivNames.register_universe_binders (ConstRef kn) ubinders;
                 kn, mkProj (Projection.make p false,mkRel 1)
 	      else
 		let ccl = subst_projection fid subst ti in
@@ -360,7 +359,6 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
 		      applist (mkConstU (kn,u),proj_args) 
                   in
                   Declare.definition_message fid;
-                  UnivNames.register_universe_binders (ConstRef kn) ubinders;
 		    kn, constr_fip
                 with Type_errors.TypeError (ctx,te) ->
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) 
@@ -443,7 +441,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
   let map i (_, _, _, fieldimpls, fields, is_coe, coers) =
     let rsp = (kn, i) in (* This is ind path of idstruc *)
     let cstr = (rsp, 1) in
-    let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in
+    let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
     let build = ConstructRef cstr in
     let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
     let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in
@@ -496,9 +494,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
       in
       let cref = ConstRef cst in
       Impargs.declare_manual_implicits false cref [paramimpls];
-      UnivNames.register_universe_binders cref ubinders;
       Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
-      UnivNames.register_universe_binders (ConstRef proj_cst) ubinders;
       Classes.set_typeclass_transparency (EvalConstRef cst) false false;
       let sub = match List.hd coers with
 	| Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
diff --git a/vernac/record.mli b/vernac/record.mli
index 953d5ec3b6..04984030f7 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -20,7 +20,6 @@ val declare_projections :
   ?kind:Decl_kinds.definition_object_kind ->
   Id.t ->
   bool list ->
-  UnivNames.universe_binders ->
   Impargs.manual_implicits list ->
   Constr.rel_context ->
     (Name.t * bool) list * Constant.t option list