diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-04-28 12:49:38 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:17 +0200 |
| commit | fece24ec8aa88950477ccfed70b511f05b438718 (patch) | |
| tree | 7e6378c07a9c53e037f4ce3359779b24c73aea9b /pretyping | |
| parent | 9903b47cdccc2fe98a905ab085cb24ca36de1aed (diff) | |
Fix a bug
Incorrect environment was used when checking subtyping information of
inductive types.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ebfb1f8a7..1ef4a9f5e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -697,11 +697,12 @@ let infer_inductive_subtyping env evd mind_ent = let { Entries.mind_entry_params = params; Entries.mind_entry_inds = entries; Entries.mind_entry_polymorphic = poly; + Entries.mind_entry_cumulative = cum; Entries.mind_entry_universes = ground_uinfind; } = mind_ent in let uinfind = - if poly then + if poly && cum then begin let uctx = Univ.UInfoInd.univ_context ground_uinfind in let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in @@ -709,9 +710,9 @@ let infer_inductive_subtyping env evd mind_ent = let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env' = Environ.push_context uctx env in - let env' = Environ.push_context uctx_other env' in - let evd' = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in + let env = Environ.push_context uctx env in + let env = Environ.push_context uctx_other env in + let evd = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in let (_, _, subtyp_constraints) = List.fold_left (fun ctxs indentry -> @@ -723,7 +724,7 @@ let infer_inductive_subtyping env evd mind_ent = (fun ctxs cons -> infer_inductive_subtyping_arity_constructor ctxs dosubst cons false params) ctxs' indentry.Entries.mind_entry_lc - ) (env', evd', Univ.Constraint.empty) entries + ) (env, evd, Univ.Constraint.empty) entries in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind, Univ.UContext.make (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind), |