diff options
| author | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
| commit | a59574c8eb4bdda60e4bdd6197e8a32574985588 (patch) | |
| tree | e15e1a0f78d23cd263726d725c93a5e6ce453465 /interp/modintern.ml | |
| parent | f8d6c322783577b31cf55f8b55568ac56104202b (diff) | |
| parent | a9f0fd89cf3bb4b728eb451572a96f8599211380 (diff) | |
Merge PR #9439: Separate variance and universe fields in inductives.
Ack-by: ppedrot
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 60056dfd90..2f516f4f3c 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -107,12 +107,12 @@ 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 (nas, ctx) -> + | Entries.Polymorphic_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 - | Entries.Monomorphic_const_entry ctx -> + | Entries.Monomorphic_entry ctx -> let c = EConstr.to_constr sigma c in WithDef (fqid,(c, None)), ctx end |