diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-30 17:21:01 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-30 17:21:01 +0000 |
| commit | 4fd77a7caa5fe6e88d04ad6bb9ce4e43f5f9bd89 (patch) | |
| tree | 6d0668b08cf0d747888eef528ad42a5772f983d2 /tactics | |
| parent | 8a00bdd6d838f65601ed9006671a8afcb9a1890d (diff) | |
New tactic
setoid_replace ... with ... in ... [using relation ...]
[generate side conditions ...]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6166 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 8 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 14 | ||||
| -rw-r--r-- | tactics/setoid_replace.mli | 3 |
3 files changed, 24 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 6fac3703e..ff12e366c 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -173,6 +173,14 @@ TACTIC EXTEND SetoidReplace [ setoid_replace None c1 c2 ~new_goals:l ] | [ "Setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) ] -> [ setoid_replace (Some rel) c1 c2 ~new_goals:l ] + | [ "Setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) ] -> + [ setoid_replace_in h None c1 c2 ~new_goals:[] ] + | [ "Setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel)] -> + [ setoid_replace_in h (Some rel) c1 c2 ~new_goals:[] ] + | [ "Setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] -> + [ setoid_replace_in h None c1 c2 ~new_goals:l ] + | [ "Setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) ] -> + [ setoid_replace_in h (Some rel) c1 c2 ~new_goals:l ] END TACTIC EXTEND SetoidRewrite diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 4c5dc08b0..e1d63fe1d 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1358,7 +1358,7 @@ let general_s_rewrite lft2rgt c ~new_goals gl = | Right2Left -> relation_rewrite c2 c1 (direction,eqclause) ~new_goals gl let general_s_rewrite_in id lft2rgt c ~new_goals gl = - let eqclause,c1,c2 = analyse_hypothesis gl c in + let _,c1,c2 = analyse_hypothesis gl c in let hyp = pf_type_of gl (mkVar id) in let new_hyp = if lft2rgt then @@ -1410,3 +1410,15 @@ let setoid_replace relation c1 c2 ~new_goals gl = (replace true eq_left_to_right) (replace false eq_right_to_left) gl with Use_replace -> (!replace c1 c2) gl + +let setoid_replace_in id relation c1 c2 ~new_goals gl = + let hyp = pf_type_of gl (mkVar id) in + let new_hyp = Termops.replace_term c1 c2 hyp in + tclTHENS + (cut new_hyp) + [ (* Try to insert the new hyp at the same place *) + tclORELSE (intro_replacing id) + (tclTHEN (clear [id]) (introduction id)); + tclTHENLASTn + (setoid_replace relation c2 c1 ~new_goals) + [| exact_check (mkVar id); tclIDTAC |] ] gl diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 3b71708b4..4200ff545 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -26,6 +26,9 @@ val equiv_list : unit -> constr list val setoid_replace : constr option -> constr -> constr -> new_goals:constr list -> tactic +val setoid_replace_in : + identifier -> constr option -> constr -> constr -> new_goals:constr list -> + tactic val general_s_rewrite : bool -> constr -> new_goals:constr list -> tactic val general_s_rewrite_in : |