diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 5 |
2 files changed, 5 insertions, 4 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index eb7b28690b..d6ad598c5b 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1048,8 +1048,8 @@ module Strategies = lemmas rewrite_unif_flags lems state env avoid t ty cstr evars let reduce (r : Redexpr.red_expr) : 'a pure_strategy = - let rfn, ckind = Redexpr.reduction_of_red_expr r in - fun state env avoid t ty cstr evars -> + fun state env avoid t ty cstr evars -> + let rfn, ckind = Redexpr.reduction_of_red_expr env r in let t' = rfn env (goalevars evars) t in if eq_constr t' t then state, Some None diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c1bd8e0c97..004a93ed18 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -379,7 +379,8 @@ let reduce redexp cl goal = let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in let redexps = reduction_clause redexp cl in let tac = tclMAP (fun (where,redexp) -> - reduct_option (Redexpr.reduction_of_red_expr redexp) where) redexps in + reduct_option + (Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in match redexp with | Fold _ | Pattern _ -> with_check tac goal | _ -> tac goal @@ -552,7 +553,7 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl = match pf_lookup_hypothesis_as_renamed env ccl h with | None when red -> aux - ((fst (Redexpr.reduction_of_red_expr (Red true))) + ((fst (Redexpr.reduction_of_red_expr env (Red true))) env (project gl) ccl) | x -> x in |