diff options
| author | Pierre-Marie Pédrot | 2019-03-14 19:00:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-10 15:03:19 +0200 |
| commit | 2a79abc613bdf19b53685a40c993f964455904fe (patch) | |
| tree | c0fd8ab20f683c3141934d060852dcda0d569f00 /pretyping/evarconv.ml | |
| parent | aab47903fb2d3e0085b03d5ade94f4ae644cd76c (diff) | |
No more local reduction functions in Reductionops.
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f1506f5f59..36dc01e272 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -136,7 +136,7 @@ let flex_kind_of_term flags env evd c sk = | Cast _ | App _ | Case _ -> assert false let apprec_nohdbeta flags env evd c = - let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in + let (t,sk as appr) = Reductionops.whd_nored_state env evd (c, []) in if flags.modulo_betaiota && Stack.not_purely_applicative sk then Stack.zip evd (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd appr) @@ -496,8 +496,8 @@ let rec evar_conv_x flags env evd pbty term1 term2 = let term2 = apprec_nohdbeta flags env evd term2 in let default () = evar_eqappr_x flags env evd pbty - (whd_nored_state evd (term1,Stack.empty)) - (whd_nored_state evd (term2,Stack.empty)) + (whd_nored_state env evd (term1,Stack.empty)) + (whd_nored_state env evd (term2,Stack.empty)) in begin match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> @@ -556,7 +556,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let env' = push_rel (RelDecl.LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env' evd (c'1, Stack.empty) in - let out2, _ = whd_nored_state evd + let out2, _ = whd_nored_state env' evd (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x flags env' evd CONV out1 out2 |