diff options
| author | Gaëtan Gilbert | 2018-11-09 16:31:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-09 16:31:32 +0100 |
| commit | 1761f8ed41f3891f8b6edc0dd256cd18e47a74fb (patch) | |
| tree | 754bd11791e63df535dff44a58e126ff9330b8ea /interp/modintern.ml | |
| parent | 5d90e05b35f85607c43888b9adb0319e98a81fb4 (diff) | |
| parent | 8272c4e08f3c045a27d0bcb89a67a167625bf233 (diff) | |
Merge PR #8601: Move bound universe names to abstract contexts
Diffstat (limited to 'interp/modintern.ml')
| -rw-r--r-- | interp/modintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index 51e27299e3..60056dfd90 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -107,8 +107,8 @@ let transl_with_decl env base kind = function let c, ectx = interp_constr env sigma c in let poly = lookup_polymorphism env base kind fqid in begin match UState.check_univ_decl ~poly ectx udecl with - | Entries.Polymorphic_const_entry ctx -> - let inst, ctx = Univ.abstract_universes ctx in + | Entries.Polymorphic_const_entry (nas, ctx) -> + 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 |