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

29 files changed, 190 insertions, 160 deletions

diff --git a/checker/values.ml b/checker/values.ml
index 8f6b24ec26..e21acd8179 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -122,8 +122,7 @@ let v_cstrs =
 let v_variance = v_enum "variance" 3
 
 let v_instance = Annot ("instance", Array v_level)
-let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|]
-let v_abs_context = v_context (* only for clarity *)
+let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|]
 let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
diff --git a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh
new file mode 100644
index 0000000000..9d723dc7f2
--- /dev/null
+++ b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh
@@ -0,0 +1,11 @@
+_OVERLAY_BRANCH=name-abstract-univ-context
+
+if [ "$CI_PULL_REQUEST" = "8601" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
+
+    Elpi_CI_REF="$_OVERLAY_BRANCH"
+    Elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+    Equations_CI_REF="$_OVERLAY_BRANCH"
+    Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
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..ad91d31f87 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -36,69 +36,28 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 let empty_binders = Id.Map.empty
 
-let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders"
-
-let universe_binders_of_global ref : Id.t list =
-  try
-    let l = GlobRef.Map.find ref !universe_binders_table in l
-  with Not_found -> []
-
-let cache_ubinder (_,(ref,l)) =
-  universe_binders_table := GlobRef.Map.add ref l !universe_binders_table
-
-let subst_ubinder (subst,(ref,l as orig)) =
-  let ref' = fst (Globnames.subst_global subst ref) in
-  if ref == ref' then orig else ref', l
+let universe_binders_of_global ref : Name.t array =
+  try AUContext.names (Environ.universes_of_global (Global.env ()) ref)
+  with Not_found -> [||]
 
 let name_universe lvl =
   (** Best-effort naming from the string representation of the level. This is
       completely hackish and should be solved in upper layers instead. *)
   Id.of_string_soft (Level.to_string lvl)
 
-let discharge_ubinder (_,(ref,l)) =
-  (** Expand polymorphic binders with the section context *)
-  let info = Lib.section_segment_of_reference ref in
-  let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in
-  let map lvl = match Level.name lvl with
-    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
-      assert false
-    | Some na ->
-      try
-        let qid = Nametab.shortest_qualid_of_universe na in
-        snd (Libnames.repr_qualid qid)
-      with Not_found -> name_universe lvl
-  in
-  let l = List.map map sec_inst @ l in
-  Some (ref, l)
-
-let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj =
-  let open Libobject in
-  declare_object { (default_object "universe binder") with
-    cache_function = cache_ubinder;
-    load_function = (fun _ x -> cache_ubinder x);
-    classify_function = (fun x -> Substitute x);
-    subst_function = subst_ubinder;
-    discharge_function = discharge_ubinder;
-    rebuild_function = (fun x -> x); }
-
-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 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 LMap.find lvl revmap
-    with Not_found -> name_universe lvl
+    try Name (LMap.find lvl revmap)
+    with Not_found -> Name (name_universe lvl)
   in
-  let ubinders = Array.map_to_list map (Instance.to_array univs) in
-  if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders))
+  Array.map map (Instance.to_array inst)
 
 type univ_name_list = Names.lname list
 
 let universe_binders_with_opt_names ref names =
   let orig = universe_binders_of_global ref in
+  let orig = Array.to_list orig in
   let udecl = match names with
   | None -> orig
   | Some udecl ->
@@ -106,11 +65,14 @@ let universe_binders_with_opt_names ref names =
       List.map2 (fun orig {CAst.v = na} ->
           match na with
           | Anonymous -> orig
-          | Name id -> id) orig udecl
+          | Name id -> Name id) orig udecl
     with Invalid_argument _ ->
       let len = List.length orig in
       CErrors.user_err ~hdr:"universe_binders_with_opt_names"
         Pp.(str "Universe instance should have length " ++ int len)
   in
-  let fold i acc na = Names.Id.Map.add na (Level.var i) acc in
+  let fold i acc na = match na with
+  | Name id -> Names.Id.Map.add id (Level.var i) acc
+  | Anonymous -> acc
+  in
   List.fold_left_i fold 0 empty_binders udecl
diff --git a/engine/univNames.mli b/engine/univNames.mli
index bd4062ade4..dc669f45d6 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -19,7 +19,7 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 val empty_binders : universe_binders
 
-val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
+val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array
 
 type univ_name_list = Names.lname list
 
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
diff --git a/kernel/entries.ml b/kernel/entries.ml
index c5bcd74072..58bb782f15 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 array * Univ.UContext.t
+  | Cumulative_ind_entry of Name.t array * 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 array * 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..20c90bc05a 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,12 @@ 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 -> 
-    let (inst, auctx) = Univ.abstract_universes ctx in
+  | Polymorphic_ind_entry (nas, ctx) ->
+    let (inst, auctx) = Univ.abstract_universes nas ctx in
     let inst = Univ.make_instance_subst inst in
     (inst, Polymorphic_ind auctx)
-  | Cumulative_ind_entry cumi -> 
-    let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+  | Cumulative_ind_entry (nas, cumi) ->
+    let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi 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..35fa871b4e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -68,8 +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 ->
-    let sbst, auctx = Univ.abstract_universes uctx in
+  | Polymorphic_const_entry (nas, uctx) ->
+    let sbst, auctx = Univ.abstract_universes nas uctx in
     let sbst = Univ.make_instance_subst sbst in
     sbst, Polymorphic_const auctx
 
@@ -78,7 +78,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 +150,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
@@ -160,7 +160,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
             i.e. [trust] is always [Pure]. *)
         let () = assert (Univ.ContextSet.is_empty ctx) in
         let env = push_context ~strict:false uctx env in
-        let sbst, auctx = Univ.abstract_universes uctx in
+        let sbst, auctx = Univ.abstract_universes nas uctx in
         let sbst = Univ.make_instance_subst sbst in
         env, sbst, Polymorphic_const auctx
       in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d09b54e7ec..0edf750997 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -937,17 +937,30 @@ let hcons_universe_context = UContext.hcons
 
 module AUContext =
 struct
-  include UContext
+  type t = Names.Name.t array constrained
 
   let repr (inst, cst) =
-    (Array.mapi (fun i _l -> Level.var i) inst, cst)
+    (Array.init (Array.length inst) (fun i -> Level.var i), cst)
 
-  let pr f ?variance ctx = pr f ?variance (repr ctx)
+  let pr f ?variance ctx = UContext.pr f ?variance (repr ctx)
 
   let instantiate inst (u, cst) =
     assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
 
+  let names (nas, _) = nas
+
+  let hcons (univs, cst) =
+    (Array.map Names.Name.hcons univs, hcons_constraints cst)
+
+  let empty = ([||], Constraint.empty)
+
+  let is_empty (nas, cst) = Array.is_empty nas && Constraint.is_empty cst
+
+  let union (nas, cst) (nas', cst') = (Array.append nas nas', Constraint.union cst cst')
+
+  let size (nas, _) = Array.length nas
+
 end
 
 let hcons_abstract_universe_context = AUContext.hcons
@@ -993,7 +1006,22 @@ end
 
 let hcons_cumulativity_info = CumulativityInfo.hcons
 
-module ACumulativityInfo = CumulativityInfo
+module ACumulativityInfo =
+struct
+  type t = AUContext.t * Variance.t array
+
+  let pr prl (univs, variance) =
+    AUContext.pr prl ~variance univs
+
+  let hcons (univs, variance) = (* should variance be hconsed? *)
+    (AUContext.hcons univs, variance)
+
+  let univ_context (univs, _subtypcst) = univs
+  let variance (_univs, variance) = variance
+
+  let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
+  let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
+end
 
 let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons
 
@@ -1145,19 +1173,20 @@ let make_inverse_instance_subst i =
       LMap.empty arr
 
 let make_abstract_instance (ctx, _) = 
-  Array.mapi (fun i _l -> Level.var i) ctx
+  Array.init (Array.length ctx) (fun i -> Level.var i)
 
-let abstract_universes ctx =
+let abstract_universes nas ctx =
   let instance = UContext.instance ctx in
+  let () = assert (Int.equal (Array.length nas) (Instance.length instance)) in
   let subst = make_instance_subst instance in
   let cstrs = subst_univs_level_constraints subst 
       (UContext.constraints ctx)
   in
-  let ctx = UContext.make (instance, cstrs) in
+  let ctx = (nas, cstrs) in
   instance, ctx
 
-let abstract_cumulativity_info (univs, variance) =
-  let subst, univs = abstract_universes univs in
+let abstract_cumulativity_info nas (univs, variance) =
+  let subst, univs = abstract_universes nas univs in
   subst, (univs, variance)
 
 let rec compact_univ s vars i u =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7ac8247ca4..de7b334ae4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -336,9 +336,6 @@ sig
   val empty : t
   val is_empty : t -> bool
 
-  (** Don't use. *)
-  val instance : t -> Instance.t
-
   val size : t -> int
 
   (** Keeps the order of the instances *)
@@ -347,6 +344,9 @@ sig
   val instantiate : Instance.t -> t -> Constraint.t
   (** Generate the set of instantiated Constraint.t **)
 
+  val names : t -> Names.Name.t array
+  (** Return the names of the bound universe variables *)
+
 end
 
 (** Universe info for cumulative inductive types: A context of
@@ -466,8 +466,8 @@ val make_instance_subst : Instance.t -> universe_level_subst
 
 val make_inverse_instance_subst : Instance.t -> universe_level_subst
 
-val abstract_universes : UContext.t -> Instance.t * AUContext.t
-val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
+val abstract_universes : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t
+val abstract_cumulativity_info : Names.Name.t array -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
 (** TODO: move universe abstraction out of the kernel *)
 
 val make_abstract_instance : AUContext.t -> Instance.t
diff --git a/library/lib.ml b/library/lib.ml
index 690a4fd53d..9c13cdafdb 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -479,7 +479,24 @@ let instance_from_variable_context =
 
 let named_of_variable_context =
   List.map fst
-  
+
+let name_instance inst =
+  (** FIXME: this should probably be done at an upper level, by storing the
+      name information in the section data structure. *)
+  let map lvl = match Univ.Level.name lvl with
+    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+      assert false
+    | Some na ->
+      try
+        let qid = Nametab.shortest_qualid_of_universe na in
+        Name (Libnames.qualid_basename qid)
+      with Not_found ->
+        (** Best-effort naming from the string representation of the level.
+            See univNames.ml for a similar hack. *)
+        Name (Id.of_string_soft (Univ.Level.to_string lvl))
+  in
+  Array.map map (Univ.Instance.to_array inst)
+
 let add_section_replacement f g poly hyps =
   match !sectab with
   | [] -> ()
@@ -488,7 +505,8 @@ let add_section_replacement f g poly hyps =
     let sechyps,ctx = extract_hyps (vars,hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
     let inst = Univ.UContext.instance ctx in
-    let subst, ctx = Univ.abstract_universes ctx in
+    let nas = name_instance inst in
+    let subst, ctx = Univ.abstract_universes nas ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
     let info = {
       abstr_ctx = sechyps;
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..047f4cd080 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/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 49c292c501..178116c580 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -150,6 +150,11 @@ Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
 
 For inseccstr: Argument scope is [type_scope]
+Polymorphic insec2@{u} = Prop
+     : Type@{Set+1}
+(* u |=  *)
+
+insec2 is universe polymorphic
 Polymorphic inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
@@ -171,26 +176,26 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i UnivBinders.55 UnivBinders.56} :
-Type@{UnivBinders.55} -> Type@{i}
-(* i UnivBinders.55 UnivBinders.56 |=  *)
+axfoo@{i UnivBinders.56 UnivBinders.57} :
+Type@{UnivBinders.56} -> Type@{i}
+(* i UnivBinders.56 UnivBinders.57 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.55 UnivBinders.56} :
-Type@{UnivBinders.56} -> Type@{i}
-(* i UnivBinders.55 UnivBinders.56 |=  *)
+axbar@{i UnivBinders.56 UnivBinders.57} :
+Type@{UnivBinders.57} -> Type@{i}
+(* i UnivBinders.56 UnivBinders.57 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axbar
-axfoo' : Type@{UnivBinders.58} -> Type@{axbar'.i}
+axfoo' : Type@{UnivBinders.59} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo'
-axbar' : Type@{UnivBinders.58} -> Type@{axbar'.i}
+axbar' : Type@{UnivBinders.59} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 56474a0723..19d241d35d 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -130,6 +130,12 @@ End SomeSec.
 Print insec.
 Print insecind.
 
+Section SomeSec2.
+  Universe u.
+  Definition insec2@{} := Prop.
+End SomeSec2.
+Print insec2.
+
 Module SomeMod.
   Definition inmod@{u} := Type@{u}.
   Print inmod.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 39919a141a..b0dba2485a 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/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/lemmas.ml b/vernac/lemmas.ml
index 9019fa15d5..150f2c6ee9 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..ac84003266 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -277,12 +277,12 @@ 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
   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
@@ -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))) 
@@ -389,10 +387,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
@@ -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
@@ -480,7 +478,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
@@ -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) 
@@ -508,11 +504,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,8 +537,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 ->
-      let usubst, auctx = Univ.abstract_universes univs in
+    | Polymorphic_const_entry (nas, univs) ->
+      let usubst, auctx = Univ.abstract_universes nas univs in
       let usubst = Univ.make_instance_subst usubst in
       let map c = Vars.subst_univs_level_constr usubst c in
       let fields = Context.Rel.map map fields in
@@ -682,11 +678,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
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