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

(limited to 'kernel/term_typing.ml')

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