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