From 601ce3738253e4bb197900ee6dad271c4e3666d6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Sep 2018 14:23:25 +0200
Subject: Adding universe names to polymorphic entry instances.

---
 engine/uState.ml                                   | 19 +++++++++++----
 engine/univNames.ml                                | 17 +++++++++-----
 engine/univNames.mli                               |  2 ++
 interp/declare.ml                                  | 14 +++++------
 interp/discharge.ml                                |  6 +++--
 interp/modintern.ml                                |  2 +-
 kernel/entries.ml                                  |  6 ++---
 kernel/indtypes.ml                                 | 12 ++++++----
 kernel/safe_typing.ml                              |  2 +-
 kernel/term_typing.ml                              |  8 ++++---
 kernel/univ.ml                                     |  3 +++
 kernel/univ.mli                                    |  3 +++
 pretyping/inferCumulativity.ml                     |  4 ++--
 tactics/abstract.ml                                |  2 +-
 tactics/ind_tables.ml                              |  7 ++----
 .../misc/poly-capture-global-univs/src/evilImpl.ml |  2 +-
 vernac/classes.ml                                  | 15 ++++++------
 vernac/comAssumption.ml                            |  4 ++--
 vernac/comInductive.ml                             |  6 ++---
 vernac/lemmas.ml                                   |  2 +-
 vernac/obligations.ml                              |  7 ++----
 vernac/record.ml                                   | 27 +++++++++++-----------
 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
-- 
cgit v1.2.3


From 168af2ba6ae1facf948c7c7bee725ac0f0cd3b41 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Sep 2018 15:34:28 +0200
Subject: Force the user to provide names when generating abstract universe
 contexts.

For now this data is not stored, but the code checks that indeed the number
of names provided coincide with the instance length.

I had to reimplement the same kind of workaround hack in section handling as
the one already performed in UnivNames because the name information is not
present in the section data structure. This deserves a FIXME.
---
 interp/modintern.ml   |  2 +-
 kernel/indtypes.ml    |  6 ++----
 kernel/term_typing.ml |  6 ++----
 kernel/univ.ml        |  7 ++++---
 kernel/univ.mli       |  4 ++--
 library/lib.ml        | 22 ++++++++++++++++++++--
 vernac/record.ml      |  3 +--
 7 files changed, 32 insertions(+), 18 deletions(-)

diff --git a/interp/modintern.ml b/interp/modintern.ml
index 93aa271e8b..60056dfd90 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -108,7 +108,7 @@ let transl_with_decl env base kind = function
     let poly = lookup_polymorphism env base kind fqid in
     begin match UState.check_univ_decl ~poly ectx udecl with
       | Entries.Polymorphic_const_entry (nas, ctx) ->
-        let inst, ctx = Univ.abstract_universes ctx in
+        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/indtypes.ml b/kernel/indtypes.ml
index 2d74f99c15..20c90bc05a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -852,13 +852,11 @@ let abstract_inductive_universes iu =
   match iu with
   | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind 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, auctx) = Univ.abstract_universes nas ctx in
     let inst = Univ.make_instance_subst inst in
     (inst, Polymorphic_ind auctx)
   | 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, acumi) = Univ.abstract_cumulativity_info nas cumi in
     let inst = Univ.make_instance_subst inst in
     (inst, Cumulative_ind acumi)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 4759625e8a..35fa871b4e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -69,8 +69,7 @@ let abstract_constant_universes = function
   | Monomorphic_const_entry uctx ->
     Univ.empty_level_subst, Monomorphic_const 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, auctx = Univ.abstract_universes nas uctx in
     let sbst = Univ.make_instance_subst sbst in
     sbst, Polymorphic_const auctx
 
@@ -160,9 +159,8 @@ 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, 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 35566019a8..a8359bc4a7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1150,8 +1150,9 @@ let make_inverse_instance_subst i =
 let make_abstract_instance (ctx, _) = 
   Array.mapi (fun i _l -> Level.var i) ctx
 
-let abstract_universes ctx =
+let abstract_universes nas ctx =
   let instance = UContext.instance ctx in
+  let () = assert (Int.equal (List.length nas) (Instance.length instance)) in
   let subst = make_instance_subst instance in
   let cstrs = subst_univs_level_constraints subst 
       (UContext.constraints ctx)
@@ -1159,8 +1160,8 @@ let abstract_universes ctx =
   let ctx = UContext.make (instance, 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 bc902d8f4b..e665ed94e7 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -469,8 +469,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 list -> UContext.t -> Instance.t * AUContext.t
+val abstract_cumulativity_info : Names.Name.t list -> 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..ccf3b4d068 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_to_list 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/vernac/record.ml b/vernac/record.ml
index 5b3fb81d66..fb3ef5c09a 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -542,8 +542,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
   let univs, ctx_context, fields =
     match univs with
     | 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, 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
-- 
cgit v1.2.3


From 27048fb3ef7a10ffde1ee368f6fb7ef354431fe8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Sep 2018 16:23:28 +0200
Subject: Actually store the bound name information in the abstract universe
 context.

---
 checker/values.ml   |  3 +--
 engine/univNames.ml | 58 ++++++++---------------------------------------------
 kernel/univ.ml      | 43 ++++++++++++++++++++++++++++++---------
 kernel/univ.mli     |  3 ---
 4 files changed, 43 insertions(+), 64 deletions(-)

diff --git a/checker/values.ml b/checker/values.ml
index 8f6b24ec26..68bac10839 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" [|List 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/engine/univNames.ml b/engine/univNames.ml
index a037e577c4..5c87fed31c 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -36,51 +36,15 @@ 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
+let universe_binders_of_global ref : Name.t list =
+  try AUContext.names (Environ.universes_of_global (Global.env ()) ref)
   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 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 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 =
@@ -89,16 +53,7 @@ let compute_instance_binders inst ubinders =
   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 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))
+let register_universe_binders ref ubinders = ()
 
 type univ_name_list = Names.lname list
 
@@ -111,11 +66,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/kernel/univ.ml b/kernel/univ.ml
index a8359bc4a7..ec6dcee834 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -937,19 +937,29 @@ let hcons_universe_context = UContext.hcons
 
 module AUContext =
 struct
-  include UContext
+  type t = Names.Name.t list constrained
 
   let repr (inst, cst) =
-    (Array.mapi (fun i _l -> Level.var i) inst, cst)
+    (Array.init (List.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);
+    assert (List.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
+  let names (nas, _) = nas
+
+  let hcons (univs, cst) =
+    (List.map Names.Name.hcons univs, hcons_constraints cst)
+
+  let empty = ([], Constraint.empty)
+
+  let is_empty (nas, cst) = List.is_empty nas && Constraint.is_empty cst
+
+  let union (nas, cst) (nas', cst') = (nas @ nas', Constraint.union cst cst')
+
+  let size (nas, _) = List.length nas
 
 end
 
@@ -996,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
 
@@ -1148,7 +1173,7 @@ 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 (List.length ctx) (fun i -> Level.var i)
 
 let abstract_universes nas ctx =
   let instance = UContext.instance ctx in
@@ -1157,7 +1182,7 @@ let abstract_universes nas ctx =
   let cstrs = subst_univs_level_constraints subst 
       (UContext.constraints ctx)
   in
-  let ctx = UContext.make (instance, cstrs) in
+  let ctx = UContext.make (nas, cstrs) in
   instance, ctx
 
 let abstract_cumulativity_info nas (univs, variance) =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e665ed94e7..3788d8f90d 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 *)
-- 
cgit v1.2.3


From 6e5dd2ee8bc014d1f99cef3156a5114b11510398 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Sep 2018 17:00:10 +0200
Subject: Remove remnants of polymorphic instance name registration.

---
 engine/univNames.ml          | 2 --
 engine/univNames.mli         | 2 --
 interp/declare.ml            | 2 +-
 vernac/comProgramFixpoint.ml | 1 -
 vernac/record.ml             | 8 ++------
 vernac/record.mli            | 1 -
 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
-- 
cgit v1.2.3


From 23ef45aa14308aa0b1e1b1f6061ec9e7e7634e49 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 1 Oct 2018 13:40:45 +0200
Subject: Use arrays of names instead of lists in abstract universe names.

There is little point in having a list, as there is virtually no sharing
nor expansion of bound universe names. This representation is thus more
compact.
---
 checker/values.ml                                  |  2 +-
 engine/univNames.ml                                |  7 ++++---
 engine/univNames.mli                               |  2 +-
 kernel/entries.ml                                  |  6 +++---
 kernel/univ.ml                                     | 22 +++++++++++-----------
 kernel/univ.mli                                    |  6 +++---
 library/lib.ml                                     |  2 +-
 .../misc/poly-capture-global-univs/src/evilImpl.ml |  2 +-
 vernac/classes.ml                                  |  2 +-
 9 files changed, 26 insertions(+), 25 deletions(-)

diff --git a/checker/values.ml b/checker/values.ml
index 68bac10839..e21acd8179 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -122,7 +122,7 @@ let v_cstrs =
 let v_variance = v_enum "variance" 3
 
 let v_instance = Annot ("instance", Array v_level)
-let v_abs_context = v_tuple "abstract_universe_context" [|List v_name; v_cstrs|]
+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/engine/univNames.ml b/engine/univNames.ml
index b7ccd2372f..ad91d31f87 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -36,9 +36,9 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 let empty_binders = Id.Map.empty
 
-let universe_binders_of_global ref : Name.t list =
+let universe_binders_of_global ref : Name.t array =
   try AUContext.names (Environ.universes_of_global (Global.env ()) ref)
-  with Not_found -> []
+  with Not_found -> [||]
 
 let name_universe lvl =
   (** Best-effort naming from the string representation of the level. This is
@@ -51,12 +51,13 @@ let compute_instance_binders inst ubinders =
     try Name (LMap.find lvl revmap)
     with Not_found -> Name (name_universe lvl)
   in
-  Array.map_to_list map (Instance.to_array inst)
+  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 ->
diff --git a/engine/univNames.mli b/engine/univNames.mli
index b00c5fda95..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 compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t list
+val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array
 
 type univ_name_list = Names.lname list
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 87fa385a60..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 Name.t list * Univ.UContext.t
-  | Cumulative_ind_entry of Name.t list * 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 Name.t list * 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/univ.ml b/kernel/univ.ml
index ec6dcee834..0edf750997 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -937,29 +937,29 @@ let hcons_universe_context = UContext.hcons
 
 module AUContext =
 struct
-  type t = Names.Name.t list constrained
+  type t = Names.Name.t array constrained
 
   let repr (inst, cst) =
-    (Array.init (List.length inst) (fun i -> Level.var i), cst)
+    (Array.init (Array.length inst) (fun i -> Level.var i), cst)
 
   let pr f ?variance ctx = UContext.pr f ?variance (repr ctx)
 
   let instantiate inst (u, cst) =
-    assert (List.length u = Array.length inst);
+    assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
 
   let names (nas, _) = nas
 
   let hcons (univs, cst) =
-    (List.map Names.Name.hcons univs, hcons_constraints cst)
+    (Array.map Names.Name.hcons univs, hcons_constraints cst)
 
-  let empty = ([], Constraint.empty)
+  let empty = ([||], Constraint.empty)
 
-  let is_empty (nas, cst) = List.is_empty nas && Constraint.is_empty cst
+  let is_empty (nas, cst) = Array.is_empty nas && Constraint.is_empty cst
 
-  let union (nas, cst) (nas', cst') = (nas @ nas', Constraint.union cst cst')
+  let union (nas, cst) (nas', cst') = (Array.append nas nas', Constraint.union cst cst')
 
-  let size (nas, _) = List.length nas
+  let size (nas, _) = Array.length nas
 
 end
 
@@ -1173,16 +1173,16 @@ let make_inverse_instance_subst i =
       LMap.empty arr
 
 let make_abstract_instance (ctx, _) = 
-  Array.init (List.length ctx) (fun i -> Level.var i)
+  Array.init (Array.length ctx) (fun i -> Level.var i)
 
 let abstract_universes nas ctx =
   let instance = UContext.instance ctx in
-  let () = assert (Int.equal (List.length nas) (Instance.length instance)) 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 (nas, cstrs) in
+  let ctx = (nas, cstrs) in
   instance, ctx
 
 let abstract_cumulativity_info nas (univs, variance) =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 3788d8f90d..de7b334ae4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -344,7 +344,7 @@ sig
   val instantiate : Instance.t -> t -> Constraint.t
   (** Generate the set of instantiated Constraint.t **)
 
-  val names : t -> Names.Name.t list
+  val names : t -> Names.Name.t array
   (** Return the names of the bound universe variables *)
 
 end
@@ -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 : Names.Name.t list -> UContext.t -> Instance.t * AUContext.t
-val abstract_cumulativity_info : Names.Name.t list -> 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 ccf3b4d068..9c13cdafdb 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -495,7 +495,7 @@ let name_instance inst =
             See univNames.ml for a similar hack. *)
         Name (Id.of_string_soft (Univ.Level.to_string lvl))
   in
-  Array.map_to_list map (Univ.Instance.to_array inst)
+  Array.map map (Univ.Instance.to_array inst)
 
 let add_section_replacement f g poly hyps =
   match !sectab with
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 c4b36fb9e0..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 ([Anonymous], 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 3bac4a6555..476db06c54 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -380,7 +380,7 @@ let context poly l =
         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
-- 
cgit v1.2.3


From 028413ca6b7cec255165b32b44473c47ec835a62 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 1 Oct 2018 14:51:19 +0200
Subject: Adding an overlay for #8601.

---
 dev/ci/user-overlays/08601-name-abstract-univ-context.sh | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 dev/ci/user-overlays/08601-name-abstract-univ-context.sh

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
-- 
cgit v1.2.3


From 8272c4e08f3c045a27d0bcb89a67a167625bf233 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 8 Nov 2018 10:49:54 +0100
Subject: Add a test for bug #8939.

---
 test-suite/output/UnivBinders.out | 21 +++++++++++++--------
 test-suite/output/UnivBinders.v   |  6 ++++++
 2 files changed, 19 insertions(+), 8 deletions(-)

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.
-- 
cgit v1.2.3