diff options
| author | gareuselesinge | 2013-10-31 14:24:43 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-31 14:24:43 +0000 |
| commit | dbd94e12c9c6cb0fdecb44bfedacf0c4ae50bc3e (patch) | |
| tree | f09931dac187ca9b20bb483aee7bc9beca1e78f1 /tactics | |
| parent | b0631cba10fda88eb3518153860807b10441ef34 (diff) | |
Conv_orable made functional and part of pre_env
But for vm, the kernel should be functional now
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |