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 /vernac/record.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 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 3 |
1 files changed, 1 insertions, 2 deletions
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 |