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 /plugins/ltac | |
| 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 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3b8fb48eb0..d6b2a17882 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -478,7 +478,7 @@ let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite." let rec decompose_app_rel env evd t = (* Head normalize for compatibility with the old meta mechanism *) - let t = Reductionops.whd_betaiota evd t in + let t = Reductionops.whd_betaiota env evd t in match EConstr.kind evd t with | App (f, [||]) -> assert false | App (f, [|arg|]) -> @@ -711,7 +711,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs) ~fail:true env sigma in let evd = solve_remaining_by env sigma holes by in - let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in + let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta env evd c) in let c1 = nf c1 and c2 = nf c2 and rew_car = nf car and rel = nf rel and prf = nf prf in @@ -971,7 +971,7 @@ let unfold_match env sigma sk app = | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in - Reductionops.whd_beta sigma (mkApp (v, args)) + Reductionops.whd_beta env sigma (mkApp (v, args)) | _ -> app let is_rew_cast = function RewCast _ -> true | _ -> false |