Merge PR #8601: Move bound universe names to abstract contexts

3 files changed, 14 insertions, 12 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 7a32018c0e..fe8fc7c969 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -219,7 +219,7 @@ let cache_variable ((sp,_),o) =
       let (body, uctx), () = Future.force de.const_entry_body in
       let poly, univs = match de.const_entry_universes with
       | Monomorphic_const_entry uctx -> false, uctx
-      | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx
+      | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
       in
       let univs = Univ.ContextSet.union uctx univs in
       (** We must declare the universe constraints before type-checking the
@@ -339,7 +339,7 @@ let infer_inductive_subtyping mind_ent =
   match mind_ent.mind_entry_universes with
   | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
     mind_ent
-  | Cumulative_ind_entry cumi ->
+  | Cumulative_ind_entry (_, cumi) ->
     begin
       let env = Global.env () in
       (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
@@ -366,14 +366,14 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
     | Monomorphic_ind_entry _ ->
       (** Global constraints already defined through the inductive *)
       Monomorphic_const_entry Univ.ContextSet.empty
-    | Polymorphic_ind_entry ctx ->
-      Polymorphic_const_entry ctx
-    | Cumulative_ind_entry ctx ->
-      Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx)
+    | Polymorphic_ind_entry (nas, ctx) ->
+      Polymorphic_const_entry (nas, ctx)
+    | Cumulative_ind_entry (nas, ctx) ->
+      Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx)
   in
   let term, types = match univs with
     | Monomorphic_const_entry _ -> term, types
-    | Polymorphic_const_entry ctx ->
+    | Polymorphic_const_entry (_, ctx) ->
       let u = Univ.UContext.instance ctx in
       Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
   in
@@ -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/interp/discharge.ml b/interp/discharge.ml
index 21b2e85e8f..eeda5a6867 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -79,13 +79,15 @@ let process_inductive info modlist mib =
     | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
     | Polymorphic_ind auctx ->
       let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+      let nas = Univ.AUContext.names auctx in
       let auctx = Univ.AUContext.repr auctx in
-      subst, Polymorphic_ind_entry auctx
+      subst, Polymorphic_ind_entry (nas, auctx)
     | Cumulative_ind cumi ->
       let auctx = Univ.ACumulativityInfo.univ_context cumi in
       let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+      let nas = Univ.AUContext.names auctx in
       let auctx = Univ.AUContext.repr auctx in
-      subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx)
+      subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx)
   in
   let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
   let inds =
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 51e27299e3..60056dfd90 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -107,8 +107,8 @@ let transl_with_decl env base kind = function
     let c, ectx = interp_constr env sigma c in
     let poly = lookup_polymorphism env base kind fqid in
     begin match UState.check_univ_decl ~poly ectx udecl with
-      | Entries.Polymorphic_const_entry ctx ->
-        let inst, ctx = Univ.abstract_universes ctx in
+      | Entries.Polymorphic_const_entry (nas, ctx) ->
+        let inst, ctx = Univ.abstract_universes nas ctx in
         let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
         let c = EConstr.to_constr sigma c in
         WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty