diff options
| author | Pierre-Marie Pédrot | 2018-09-27 15:34:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-09 14:10:27 +0100 |
| commit | 168af2ba6ae1facf948c7c7bee725ac0f0cd3b41 (patch) | |
| tree | 3953f4716691915cd393ee3640e3cf6770d62701 /kernel/indtypes.ml | |
| parent | 601ce3738253e4bb197900ee6dad271c4e3666d6 (diff) | |
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.
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 6 |
1 files changed, 2 insertions, 4 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) |