Adding universe names to polymorphic entry instances.

22 files changed, 97 insertions, 73 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index aa7ec63a6f..41905feab7 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -101,13 +101,21 @@ let context ctx = Univ.ContextSet.to_context ctx.uctx_local
 
 let const_univ_entry ~poly uctx =
   let open Entries in
-  if poly then Polymorphic_const_entry (context uctx)
+  if poly then
+    let (binders, _) = uctx.uctx_names in
+    let uctx = context uctx in
+    let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+    Polymorphic_const_entry (nas, uctx)
   else Monomorphic_const_entry (context_set uctx)
 
 (* does not support cumulativity since you need more info *)
 let ind_univ_entry ~poly uctx =
   let open Entries in
-  if poly then Polymorphic_ind_entry (context uctx)
+  if poly then
+    let (binders, _) = uctx.uctx_names in
+    let uctx = context uctx in
+    let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+    Polymorphic_ind_entry (nas, uctx)
   else Monomorphic_ind_entry (context_set uctx)
 
 let of_context_set ctx = { empty with uctx_local = ctx }
@@ -394,8 +402,11 @@ let check_univ_decl ~poly uctx decl =
   let ctx =
     let names = decl.univdecl_instance in
     let extensible = decl.univdecl_extensible_instance in
-    if poly
-    then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx)
+    if poly then
+      let (binders, _) = uctx.uctx_names in
+      let uctx = universe_context ~names ~extensible uctx in
+      let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
+      Entries.Polymorphic_const_entry (nas, uctx)
     else
       let () = check_universe_context_set ~names ~extensible uctx in
       Entries.Monomorphic_const_entry uctx.uctx_local
diff --git a/engine/univNames.ml b/engine/univNames.ml
index a71f9c5736..a037e577c4 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -81,18 +81,23 @@ let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj =
     discharge_function = discharge_ubinder;
     rebuild_function = (fun x -> x); }
 
+let compute_instance_binders inst ubinders =
+  let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
+  let map lvl =
+    try Name (LMap.find lvl revmap)
+    with Not_found -> Name (name_universe lvl)
+  in
+  Array.map_to_list map (Instance.to_array inst)
+
 let register_universe_binders ref ubinders =
   (** TODO: change the API to register a [Name.t list] instead. This is the last
       part of the code that depends on the internal representation of names in
       abstract contexts, but removing it requires quite a rework of the
       callers. *)
   let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in
-  let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
-  let map lvl =
-    try LMap.find lvl revmap
-    with Not_found -> name_universe lvl
-  in
-  let ubinders = Array.map_to_list map (Instance.to_array univs) in
+  let ubinders = compute_instance_binders univs ubinders in
+  (** FIXME: the function above always generate names but this may change *)
+  let ubinders = List.map (function Name id -> id | Anonymous -> assert false) ubinders in
   if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders))
 
 type univ_name_list = Names.lname list
diff --git a/engine/univNames.mli b/engine/univNames.mli
index bd4062ade4..634db9581c 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -19,6 +19,8 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 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
diff --git a/interp/declare.ml b/interp/declare.ml
index 7a32018c0e..29e777d0c6 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
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..93aa271e8b 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -107,7 +107,7 @@ 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 ->
+      | Entries.Polymorphic_const_entry (nas, ctx) ->
         let inst, ctx = Univ.abstract_universes 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
diff --git a/kernel/entries.ml b/kernel/entries.ml
index c5bcd74072..87fa385a60 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -30,8 +30,8 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 
 type inductive_universes =
   | Monomorphic_ind_entry of Univ.ContextSet.t
-  | Polymorphic_ind_entry of Univ.UContext.t
-  | Cumulative_ind_entry of Univ.CumulativityInfo.t
+  | Polymorphic_ind_entry of Name.t list * Univ.UContext.t
+  | Cumulative_ind_entry of Name.t list * Univ.CumulativityInfo.t
 
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
@@ -60,7 +60,7 @@ type 'a const_entry_body = 'a proof_output Future.computation
 
 type constant_universes_entry =
   | Monomorphic_const_entry of Univ.ContextSet.t
-  | Polymorphic_const_entry of Univ.UContext.t
+  | Polymorphic_const_entry of Name.t list * Univ.UContext.t
 
 type 'a in_constant_universes_entry = 'a * constant_universes_entry
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0346026aa4..2d74f99c15 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -268,8 +268,8 @@ let typecheck_inductive env mie =
   let env' =
     match mie.mind_entry_universes with
     | Monomorphic_ind_entry ctx -> push_context_set ctx env
-    | Polymorphic_ind_entry ctx -> push_context ctx env
-    | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
+    | Polymorphic_ind_entry (_, ctx) -> push_context ctx env
+    | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env
   in
   let env_params = check_context env' mie.mind_entry_params in
   let paramsctxt = mie.mind_entry_params in
@@ -407,7 +407,7 @@ let typecheck_inductive env mie =
     match mie.mind_entry_universes with
     | Monomorphic_ind_entry _ -> ()
     | Polymorphic_ind_entry _ -> ()
-    | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds
+    | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds
   in (env_arities, env_ar_par, paramsctxt, inds)
 
 (************************************************************************)
@@ -851,12 +851,14 @@ let compute_projections (kn, i as ind) mib =
 let abstract_inductive_universes iu =
   match iu with
   | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
-  | Polymorphic_ind_entry ctx -> 
+  | Polymorphic_ind_entry (nas, ctx) ->
+    let () = assert (Int.equal (List.length nas) (UContext.size ctx)) in
     let (inst, auctx) = Univ.abstract_universes ctx in
     let inst = Univ.make_instance_subst inst in
     (inst, Polymorphic_ind auctx)
-  | Cumulative_ind_entry cumi -> 
+  | Cumulative_ind_entry (nas, cumi) ->
     let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+    let () = assert (Int.equal (List.length nas) (Instance.length inst)) in
     let inst = Univ.make_instance_subst inst in
     (inst, Cumulative_ind acumi)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8b11851bbb..df10398b2f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -682,7 +682,7 @@ let constant_entry_of_side_effect cb u =
     | Monomorphic_const uctx ->
       Monomorphic_const_entry uctx
     | Polymorphic_const auctx ->
-      Polymorphic_const_entry (Univ.AUContext.repr auctx)
+      Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
   in
   let pt =
     match cb.const_body, u with
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index fb1b3e236c..4759625e8a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -68,7 +68,8 @@ let feedback_completion_typecheck =
 let abstract_constant_universes = function
   | Monomorphic_const_entry uctx ->
     Univ.empty_level_subst, Monomorphic_const uctx
-  | Polymorphic_const_entry uctx ->
+  | Polymorphic_const_entry (nas, uctx) ->
+    let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in
     let sbst, auctx = Univ.abstract_universes uctx in
     let sbst = Univ.make_instance_subst sbst in
     sbst, Polymorphic_const auctx
@@ -78,7 +79,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
     | ParameterEntry (ctx,(t,uctx),nl) ->
       let env = match uctx with
         | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
-        | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
+        | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env
       in
       let j = infer env t in
       let usubst, univs = abstract_constant_universes uctx in
@@ -150,7 +151,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         let ctx = Univ.ContextSet.union univs ctx in
         let env = push_context_set ~strict:true ctx env in
         env, Univ.empty_level_subst, Monomorphic_const ctx
-      | Polymorphic_const_entry uctx ->
+      | Polymorphic_const_entry (nas, uctx) ->
         (** Ensure not to generate internal constraints in polymorphic mode.
             The only way for this to happen would be that either the body
             contained deferred universes, or that it contains monomorphic
@@ -159,6 +160,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
             unconditionally export side-effects from polymorphic definitions,
             i.e. [trust] is always [Pure]. *)
         let () = assert (Univ.ContextSet.is_empty ctx) in
+        let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in
         let env = push_context ~strict:false uctx env in
         let sbst, auctx = Univ.abstract_universes uctx in
         let sbst = Univ.make_instance_subst sbst in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d09b54e7ec..35566019a8 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -948,6 +948,9 @@ struct
     assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
 
+  (** FIXME: Actually store this information in the type *)
+  let names (u, _) = Array.map_to_list (fun _ -> Names.Anonymous) u
+
 end
 
 let hcons_abstract_universe_context = AUContext.hcons
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7ac8247ca4..bc902d8f4b 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -347,6 +347,9 @@ sig
   val instantiate : Instance.t -> t -> Constraint.t
   (** Generate the set of instantiated Constraint.t **)
 
+  val names : t -> Names.Name.t list
+  (** Return the names of the bound universe variables *)
+
 end
 
 (** Universe info for cumulative inductive types: A context of
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index 422a05c19a..9762d0f1d9 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -188,7 +188,7 @@ let infer_inductive env mie =
     match mie.mind_entry_universes with
     | Monomorphic_ind_entry _
     | Polymorphic_ind_entry _ as univs -> univs
-    | Cumulative_ind_entry cumi ->
+    | Cumulative_ind_entry (nas, cumi) ->
       let uctx = CumulativityInfo.univ_context cumi in
       let uarray = Instance.to_array @@ UContext.instance uctx in
       let env = Environ.push_context uctx env in
@@ -207,6 +207,6 @@ let infer_inductive env mie =
           entries
       in
       let variances = Array.map (fun u -> LMap.find u variances) uarray in
-      Cumulative_ind_entry (CumulativityInfo.make (uctx, variances))
+      Cumulative_ind_entry (nas, CumulativityInfo.make (uctx, variances))
   in
   { mie with mind_entry_universes = univs }
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 2b4d9a7adf..3c262de910 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -148,7 +148,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   let cst = Impargs.with_implicit_protection cst () in
   let inst = match const.Entries.const_entry_universes with
   | Entries.Monomorphic_const_entry _ -> EInstance.empty
-  | Entries.Polymorphic_const_entry ctx ->
+  | Entries.Polymorphic_const_entry (_, ctx) ->
     (** We mimick what the kernel does, that is ensuring that no additional
         constraints appear in the body of polymorphic constants. Ideally this
         should be enforced statically. *)
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index b81967c781..a53e3bf20d 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -118,15 +118,12 @@ let compute_name internal id =
   | InternalTacticRequest ->
       Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
 
-let define internal id c p univs =
+let define internal id c poly univs =
   let fd = declare_constant ~internal in
   let id = compute_name internal id in
   let ctx = UState.minimize univs in
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
-  let univs =
-    if p then Polymorphic_const_entry (UState.context ctx)
-    else Monomorphic_const_entry (UState.context_set ctx)
-  in
+  let univs = UState.const_univ_entry ~poly ctx in
   let entry = {
     const_entry_body =
       Future.from_val ((c,Univ.ContextSet.empty),
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
index 6d8ce7c5d7..c4b36fb9e0 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -15,7 +15,7 @@ let evil t f =
   let tc = mkConst tc in
 
   let fe = Declare.definition_entry
-      ~univs:(Polymorphic_const_entry (UContext.make (Instance.of_array [|u|],Constraint.empty)))
+      ~univs:(Polymorphic_const_entry ([Anonymous], UContext.make (Instance.of_array [|u|],Constraint.empty)))
       ~types:(Term.mkArrow tc tu)
       (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1))
   in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index f4b0015851..3bac4a6555 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -370,25 +370,24 @@ let context poly l =
       user_err Pp.(str "Anonymous variables not allowed in contexts.")
   in
   let univs =
-    let uctx = Evd.universe_context_set sigma in
     match ctx with
     | [] -> assert false
-    | [_] ->
-      if poly
-      then Polymorphic_const_entry (Univ.ContextSet.to_context uctx)
-      else Monomorphic_const_entry uctx
+    | [_] -> Evd.const_univ_entry ~poly sigma
     | _::_::_ ->
+      (** TODO: explain this little belly dance *)
       if Lib.sections_are_opened ()
       then
         begin
+          let uctx = Evd.universe_context_set sigma in
           Declare.declare_universe_context poly uctx;
-          if poly then Polymorphic_const_entry Univ.UContext.empty
+          if poly then Polymorphic_const_entry ([], Univ.UContext.empty)
           else Monomorphic_const_entry Univ.ContextSet.empty
         end
-      else if poly
-      then Polymorphic_const_entry (Univ.ContextSet.to_context uctx)
+      else if poly then
+        Evd.const_univ_entry ~poly sigma
       else
         begin
+          let uctx = Evd.universe_context_set sigma in
           Declare.declare_universe_context poly uctx;
           Monomorphic_const_entry Univ.ContextSet.empty
         end
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index e990f0cd15..8707121306 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -47,7 +47,7 @@ match local with
 | Discharge when Lib.sections_are_opened () ->
   let ctx = match ctx with
     | Monomorphic_const_entry ctx -> ctx
-    | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx
+    | Polymorphic_const_entry (_, ctx) -> Univ.ContextSet.of_context ctx
   in
   let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
   let _ = declare_variable ident decl in
@@ -79,7 +79,7 @@ match local with
   let () = if do_instance then Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr ~local p in
   let inst = match ctx with
-    | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+    | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
     | Monomorphic_const_entry _ -> Univ.Instance.empty
   in
     (gr,inst,Lib.is_modtype_strict ())
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5ff3032ec4..0c39458a57 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -450,10 +450,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   in
   let univs =
     match uctx with
-    | Polymorphic_const_entry uctx ->
+    | Polymorphic_const_entry (nas, uctx) ->
       if cum then
-        Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx)
-      else Polymorphic_ind_entry uctx
+        Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx)
+      else Polymorphic_ind_entry (nas, uctx)
     | Monomorphic_const_entry uctx ->
       Monomorphic_ind_entry uctx
   in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 8aa459729c..602314eec3 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -228,7 +228,7 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,
       | Discharge ->
           let impl = false in (* copy values from Vernacentries *)
           let univs = match univs with
-            | Polymorphic_const_entry univs ->
+            | Polymorphic_const_entry (_, univs) ->
               (* What is going on here? *)
               Univ.ContextSet.of_context univs
             | Monomorphic_const_entry univs -> univs
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 97ed43c5f4..c2805674e4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -667,7 +667,7 @@ let declare_obligation prg obl body ty uctx =
       if not opaque then add_hint (Locality.make_section_locality None) prg constant;
       definition_message obl.obl_name;
       let body = match uctx with
-        | Polymorphic_const_entry uctx ->
+        | Polymorphic_const_entry (_, uctx) ->
           Some (DefinedObl (constant, Univ.UContext.instance uctx))
         | Monomorphic_const_entry _ ->
           Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx))
@@ -1004,10 +1004,7 @@ and solve_obligation_by_tac prg obls i tac =
               solve_by_tac obl.obl_name (evar_of_obligation obl) tac
                 (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
             in
-            let uctx = if pi2 prg.prg_kind
-              then Polymorphic_const_entry (UState.context ctx)
-              else Monomorphic_const_entry (UState.context_set ctx)
-            in
+            let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
             let prg = {prg with prg_ctx = ctx} in
             let def, obl' = declare_obligation prg obl t ty uctx in
               obls.(i) <- obl';
diff --git a/vernac/record.ml b/vernac/record.ml
index 7a4c38e972..5b3fb81d66 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -282,7 +282,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
   let u = match ctx with
-    | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+    | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
     | Monomorphic_const_entry ctx -> Univ.Instance.empty
   in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
@@ -389,10 +389,10 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
     match univs with
     | Monomorphic_ind_entry ctx ->
       false, Monomorphic_const_entry Univ.ContextSet.empty
-    | Polymorphic_ind_entry ctx ->
-      true, Polymorphic_const_entry ctx
-    | Cumulative_ind_entry cumi ->
-      true, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
+    | Polymorphic_ind_entry (nas, ctx) ->
+      true, Polymorphic_const_entry (nas, ctx)
+    | Cumulative_ind_entry (nas, cumi) ->
+      true, Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context cumi)
   in
   let binder_name =
     match name with
@@ -480,7 +480,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
 	(DefinitionEntry class_entry, IsDefinition Definition)
       in
       let inst, univs = match univs with
-        | Polymorphic_const_entry uctx -> Univ.UContext.instance uctx, univs
+        | Polymorphic_const_entry (_, uctx) -> Univ.UContext.instance uctx, univs
         | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty
       in
       let cstu = (cst, inst) in
@@ -508,11 +508,11 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
     | _ ->
        let univs =
          match univs with
-         | Polymorphic_const_entry univs ->
+         | Polymorphic_const_entry (nas, univs) ->
            if cum then
-             Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
+             Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
            else
-             Polymorphic_ind_entry univs
+             Polymorphic_ind_entry (nas, univs)
          | Monomorphic_const_entry univs ->
            Monomorphic_ind_entry univs
        in
@@ -541,7 +541,8 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
   in
   let univs, ctx_context, fields =
     match univs with
-    | Polymorphic_const_entry univs ->
+    | Polymorphic_const_entry (nas, univs) ->
+      let () = assert (Int.equal (List.length nas) (Univ.UContext.size univs)) in
       let usubst, auctx = Univ.abstract_universes univs in
       let usubst = Univ.make_instance_subst usubst in
       let map c = Vars.subst_univs_level_constr usubst c in
@@ -682,11 +683,11 @@ let definition_structure udecl kind ~template cum poly finite records =
     let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
       let univs =
         match univs with
-        | Polymorphic_const_entry univs ->
+        | Polymorphic_const_entry (nas, univs) ->
           if cum then
-            Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
+            Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
           else
-            Polymorphic_ind_entry univs
+            Polymorphic_ind_entry (nas, univs)
         | Monomorphic_const_entry univs ->
           Monomorphic_ind_entry univs
       in