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/evarsolve.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/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 34684e4a34..348d7c0b2f 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -633,7 +633,7 @@ let solve_pattern_eqn env sigma l c = l c in (* Warning: we may miss some opportunity to eta-reduce more since c' is not in normal form *) - shrink_eta c' + shrink_eta env c' (*****************************************) (* Refining/solving unification problems *) @@ -1632,7 +1632,7 @@ let rec invert_definition unify flags choose imitate_defs map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) imitate envk t in - let rhs = whd_beta evd rhs (* heuristic *) in + let rhs = whd_beta env evd rhs (* heuristic *) in let fast rhs = let filter_ctxt = evar_filtered_context evi in let names = ref Id.Set.empty in @@ -1758,7 +1758,7 @@ let reconsider_unif_constraints unify flags evd = let solve_simple_eqn unify flags ?(choose=false) ?(imitate_defs=true) env evd (pbty,(evk1,args1 as ev1),t2) = try - let t2 = whd_betaiota evd t2 in (* includes whd_evar *) + let t2 = whd_betaiota env evd t2 in (* includes whd_evar *) let evd = evar_define unify flags ~choose ~imitate_defs env evd pbty ev1 t2 in reconsider_unif_constraints unify flags evd with |