diff options
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 |