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.
---
 vernac/record.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'vernac')

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