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.
---
 kernel/indtypes.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'kernel/indtypes.ml')

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