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

1 files changed, 13 insertions, 1 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 4c5dc08b0d..e1d63fe1dc 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