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 /interp/modintern.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 'interp/modintern.ml')
| -rw-r--r-- | interp/modintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index 93aa271e8b..60056dfd90 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -108,7 +108,7 @@ let transl_with_decl env base kind = function let poly = lookup_polymorphism env base kind fqid in begin match UState.check_univ_decl ~poly ectx udecl with | Entries.Polymorphic_const_entry (nas, ctx) -> - let inst, ctx = Univ.abstract_universes ctx in + let inst, ctx = Univ.abstract_universes nas ctx in let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in let c = EConstr.to_constr sigma c in WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty |