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.

4 files changed, 10 insertions, 13 deletions

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