From f208cfc23dc997fd0409a9309628bc1804287d7d Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Thu, 30 Sep 2004 10:56:57 +0000
Subject: setoid_replace E1 with E2

now replaces E1 with E2 either generating the goal E1 R E2
or the goal E2 R E1 (as expected).

Note: the relation R is guessed when more than one is applicable.
This is not very nice, since it can guess the wrong one.

Since making the tactic compute R requires much code refactoring, I
would suggest the user to always use cutrewrite in place of setoid_rewrite.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6162 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 3e605b17f6..7e22f8e5ee 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1349,12 +1349,17 @@ let setoid_replace c1 c2 ~new_goals gl =
       Relation sa -> sa
     | Leibniz _ -> raise Use_replace
   in
-   let eq = mkApp (relation.rel_aeq, [| c1 ; c2 |]) in
+   let eq_left_to_right = mkApp (relation.rel_aeq, [| c1 ; c2 |]) in
+   let eq_right_to_left = mkApp (relation.rel_aeq, [| c2 ; c1 |]) in
+   let replace dir eq =
     tclTHENS (assert_tac false Anonymous eq)
       [onLastHyp (fun id ->
         tclTHEN
-          (general_s_rewrite true (mkVar id) ~new_goals)
+          (general_s_rewrite dir (mkVar id) ~new_goals)
           (clear [id]));
-       Tacticals.tclIDTAC] gl
+       Tacticals.tclIDTAC]
+   in
+    tclORELSE
+     (replace true eq_left_to_right) (replace false eq_right_to_left) gl
  with
   Use_replace -> (!replace c1 c2) gl
-- 
cgit v1.2.3