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

4 files changed, 28 insertions, 6 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 :
diff --git a/test-suite/success/setoid_test2.v8 b/test-suite/success/setoid_test2.v8
index 86f54406e..65b3973ed 100644
--- a/test-suite/success/setoid_test2.v8
+++ b/test-suite/success/setoid_test2.v8
@@ -50,10 +50,9 @@ Require Export Setoid.
     nessuna marcatura viene trovata
 
   Implementare:
-   -1. user-defined subrelations && user-proved subrelations
-    0. trucco di Bruno
-    2. setoid_replace ... with ... in ...
-    4. [setoid_]symmetry, [setoid_]reflexivity, [setoid_]transitivity (?!?)
+   -2. user-defined subrelations && user-proved subrelations
+   -1. trucco di Bruno
+    0. [setoid_]symmetry, [setoid_]reflexivity, [setoid_]transitivity (?!?)
 
   Sorgenti di inefficacia:
     1. scelta del setoide di default per un sostegno: per farlo velocemente
@@ -88,7 +87,7 @@ Require Export Setoid.
        l'uguaglianza di Leibniz. (Se entrambi sono uguaglianze di Leibniz
        allora il setoide e' una semplice funzione).
   ?10. [setoid_]rewrite ... in ...
-       setoid_replace ... in
+       setoid_replace ... in ...
        [setoid_]reflexivity???
        [setoid_]transitivity???
        [setoid_]symmetry???