New tactic [setoid_]rewrite ... in ... [generate side conditions ...].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6165 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 35 insertions, 5 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 05f92985ba..eb90fa213e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -97,7 +97,9 @@ let general_rewrite_in lft2rgt id (c,l) gl =
   let _,t = splay_prod env sigma ctype in
   match match_with_equation t with
     | None -> (* Do not deal with setoids yet *) 
-        error "The term provided does not end with an equation" 
+	if l = NoBindings
+	then general_s_rewrite_in id lft2rgt c [] gl
+	else error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
         let hdcncls = string_of_inductive hdcncl in 
 	let suffix =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1457f09daa..6fac3703e5 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -180,6 +180,10 @@ TACTIC EXTEND SetoidRewrite
    -> [ general_s_rewrite b c ~new_goals:[] ]
  | [ "Setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ]
    -> [ general_s_rewrite b c ~new_goals:l ]
+ | [ "Setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] ->
+      [ general_s_rewrite_in h b c ~new_goals:[] ]
+ | [ "Setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] ->
+      [ general_s_rewrite_in h b c ~new_goals:l ]
 END
 
 VERNAC COMMAND EXTEND AddSetoid1
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 42cee320a4..4c5dc08b0d 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1339,8 +1339,7 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
    Use_rewrite ->
     !general_rewrite (input_direction = Left2Right) (snd hyp) gl
 
-let general_s_rewrite lft2rgt c ~new_goals gl =
- let direction = if lft2rgt then Left2Right else Right2Left in
+let analyse_hypothesis gl c =
  let ctype = pf_type_of gl c in
  let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
  let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
@@ -1348,11 +1347,34 @@ let general_s_rewrite lft2rgt c ~new_goals gl =
    | [c1;c2] -> (c1, c2)
    | x::y::z -> get_last_two (y::z)
    | _ -> error "The term provided is not an equivalence" in
- let (c1,c2) = get_last_two args in
+ let c1,c2 = get_last_two args in
+  eqclause,c1,c2
+
+let general_s_rewrite lft2rgt c ~new_goals gl =
+ let direction = if lft2rgt then Left2Right else Right2Left in
+ let eqclause,c1,c2 = analyse_hypothesis gl c in
   match direction with
      Left2Right -> relation_rewrite c1 c2 (direction,eqclause) ~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 hyp = pf_type_of gl (mkVar id) in
+ let new_hyp =
+  if lft2rgt then
+   Termops.replace_term c1 c2 hyp
+  else
+   Termops.replace_term c2 c1 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));
+     tclTHENLAST
+      (general_s_rewrite (not lft2rgt) c ~new_goals)
+      (exact_check (mkVar id))] gl
+
 exception Use_replace
 
 (*CSC: still setoid in the name *)
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index d815954ec4..3b71708b4a 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -11,7 +11,7 @@
 open Term
 open Proof_type
 open Topconstr
-
+open Names
 
 type morphism_signature = (bool option * constr_expr) list * constr_expr
 
@@ -28,6 +28,8 @@ val setoid_replace :
  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 :
+ identifier -> bool -> constr -> new_goals:constr list -> tactic
 
 val add_relation :
  constr_expr -> constr_expr -> constr_expr option -> constr_expr option -> unit