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/ssrmatching | |
| 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/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index adaf7c8cc1..e004613ef3 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -405,7 +405,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = (* p_origin can be passed to obtain a better error message *) let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = let k, f, a = - let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in + let f, a = Reductionops.whd_betaiota_stack env ise (EConstr.of_constr p) in let f = EConstr.Unsafe.to_constr f in let a = List.map EConstr.Unsafe.to_constr a in match kind f with |