+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no

InType) for  "replace <c1> with  <c2>" and "replace c1"  and partially
for  "autorewrite".   
+ Adding  a  "by  tactic"  optional argument  to "setoid_replace".  
+ Fixing bug #1207
+ Add new test files for syntax change and updating doc.
+ Moving argument tactic extensions from extratactics to extraargs


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

9 files changed, 347 insertions, 209 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 29ae191b39..d513653f5b 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -60,11 +60,11 @@ type raw_rew_rule = constr * bool * raw_tactic_expr
 
 (* Applies all the rules of one base *)
 let one_base general_rewrite_maybe_in tac_main bas =
-  let lrul = 
-    try 
+  let lrul =
+    try
       Stringmap.find bas !rewtab
-    with Not_found -> 
-      errorlabstrm "AutoRewrite" 
+    with Not_found ->
+      errorlabstrm "AutoRewrite"
         (str ("Rewriting base "^(bas)^" does not exist"))
   in
   let lrul = List.map (fun (c,_,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in
@@ -74,16 +74,19 @@ let one_base general_rewrite_maybe_in tac_main bas =
 	  (tclTHENSFIRSTn (general_rewrite_maybe_in dir csr) [|tac_main|] tc)))
       tclIDTAC lrul))
 
+
+
 (* The AutoRewrite tactic *)
 let autorewrite tac_main lbas =
   tclREPEAT_MAIN (tclPROGRESS
     (List.fold_left (fun tac bas -> 
        tclTHEN tac (one_base general_rewrite tac_main bas)) tclIDTAC lbas))
 
-let autorewrite_in id tac_main lbas gl =
+let autorewrite_mutlti_in idl tac_main lbas : tactic =
+  fun gl -> 
  (* let's check at once if id exists (to raise the appropriate error) *)
- let _ = Tacmach.pf_get_hyp gl id in
- let general_rewrite_in =
+ let _ = List.map (Tacmach.pf_get_hyp gl) idl in
+ let general_rewrite_in id =
   let id = ref id in
   let to_be_cleared = ref false in
    fun dir cstr gl ->
@@ -117,10 +120,51 @@ let autorewrite_in id tac_main lbas gl =
           | _ -> assert false) (* there must be at least an hypothesis *)
      | _ -> assert false (* rewriting cannot complete a proof *)
  in
+ tclMAP (fun id -> 
   tclREPEAT_MAIN (tclPROGRESS
     (List.fold_left (fun tac bas -> 
-       tclTHEN tac (one_base general_rewrite_in tac_main bas)) tclIDTAC lbas))
-   gl
+       tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) tclIDTAC lbas)))
+   idl gl
+
+let autorewrite_in id = autorewrite_mutlti_in [id]
+
+let gen_auto_multi_rewrite tac_main lbas cl = 
+  let try_do_hyps treat_id l = 
+    autorewrite_mutlti_in (List.map treat_id l) tac_main lbas
+  in 
+  if cl.concl_occs <> [] then 
+    error "The \"at\" syntax isn't available yet for the autorewrite tactic"
+  else 
+    let compose_tac t1 t2 = 
+      match cl.onhyps with 
+	| Some [] -> t1 
+	| _ ->      tclTHENFIRST t1 t2
+    in
+    compose_tac
+	(if cl.onconcl then autorewrite tac_main lbas else tclIDTAC)
+	(match cl.onhyps with 
+	   | Some l -> try_do_hyps (fun ((_,id),_) -> id) l
+	   | None -> 
+	       fun gl -> 
+		 (* try to rewrite in all hypothesis 
+		    (except maybe the rewritten one) *)
+		 let ids =  Tacmach.pf_ids_of_hyps gl
+		 in try_do_hyps (fun id -> id)  ids gl)
+
+let auto_multi_rewrite = gen_auto_multi_rewrite Refiner.tclIDTAC
+
+let auto_multi_rewrite_with tac_main lbas cl gl = 
+  match cl.Tacexpr.onconcl,cl.Tacexpr.onhyps with 
+    | false,Some [_] | true,Some [] | false,Some [] ->   
+	(* autorewrite with .... in clause using tac n'est sur que 
+	   si clause reprensente soit le but soit UNE hypothse 
+	*)
+	gen_auto_multi_rewrite tac_main  lbas cl gl
+    | _ -> 
+	    Util.errorlabstrm "autorewrite" 
+	      (str "autorewrite .. in .. using can only be used either with a unique hypothesis or" ++
+		 str " on the conclusion")
+
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index cc4c5ed37b..f0557f9d30 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -22,4 +22,9 @@ val add_rew_rules : string -> raw_rew_rule list -> unit
 val autorewrite : tactic -> string list -> tactic
 val autorewrite_in : Names.identifier -> tactic -> string list -> tactic
 
+
+val auto_multi_rewrite : string list -> Tacticals.clause -> tactic
+
+val auto_multi_rewrite_with : tactic -> string list -> Tacticals.clause -> tactic
+
 val print_rewrite_hintdb : string -> unit
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 97ed5349e1..595243eae1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -134,7 +134,7 @@ let general_multi_rewrite l2r c cl =
 	  (try_do_hyps l)
   in 
   if cl.concl_occs <> [] then 
-    error "The \"at\" syntax isn't available yet for the rewrite tactic"
+    error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
   else 
     tclTHENFIRST 
       (if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC)
@@ -182,7 +182,12 @@ let rewriteRL_clause = function
    tac : Used to prove the equality c1 = c2 
    gl : goal *)
 
-let abstract_replace clause c2 c1 unsafe tac gl =
+let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = 
+  let try_prove_eq = 
+    match try_prove_eq_opt with 
+      | None -> tclIDTAC
+      | Some tac ->  tclTRY (tclCOMPLETE tac)
+  in
   let t1 = pf_type_of gl c1 
   and t2 = pf_type_of gl c2 in
   if unsafe or (pf_conv_x gl t1 t2) then
@@ -192,34 +197,28 @@ let abstract_replace clause c2 c1 unsafe tac gl =
     tclTHENS (assert_tac false Anonymous eq)
       [onLastHyp (fun id -> 
 	tclTHEN 
-	  (tclTRY (rewriteRL_clause clause (mkVar id,NoBindings)))
+	  (tclTRY (general_multi_rewrite false (mkVar id,NoBindings) clause))
 	  (clear [id]));
        tclFIRST
 	 [assumption;
 	  tclTHEN (apply sym) assumption;
-	  tclTRY (tclCOMPLETE tac)
+	  try_prove_eq
 	 ]
       ] gl
   else
     error "terms do not have convertible types"
+  
 
+let replace c2 c1 gl = multi_replace onConcl c2 c1 false None gl
 
-let replace c2 c1 gl = abstract_replace None c2 c1 false tclIDTAC gl
-
-let replace_in id c2 c1 gl = abstract_replace (Some id) c2 c1 false tclIDTAC gl
+let replace_in id c2 c1 gl = multi_replace (onHyp id) c2 c1 false None gl
 
-let replace_by c2 c1 tac gl = abstract_replace None c2 c1 false tac gl
+let replace_by c2 c1 tac gl = multi_replace onConcl c2 c1 false (Some tac) gl
 
-let replace_in_by id c2 c1 tac gl = abstract_replace (Some id) c2 c1 false tac gl
+let replace_in_by id c2 c1 tac gl = multi_replace (onHyp id) c2 c1 false (Some tac) gl
 
-
-let new_replace c2 c1 id tac_opt gl = 
-  let tac = 
-    match tac_opt with 
-      | Some tac -> tac 
-      | _ -> tclIDTAC
-  in
-  abstract_replace id c2 c1 false tac gl
+let replace_in_clause_maybe_by c2 c1 cl tac_opt gl = 
+  multi_replace cl c2 c1 false tac_opt gl
 
 (* End of Eduardo's code. The rest of this file could be improved
    using the functions match_with_equation, etc that I defined
@@ -1147,28 +1146,10 @@ let subst_all gl =
   let ids = list_uniquize ids in
   subst ids gl
 
+
 (* Rewrite the first assumption for which the condition faildir does not fail 
    and gives the direction of the rewrite *)
 
-let rewrite_assumption_cond faildir gl =
-   let rec arec = function
-      | [] -> error "No such assumption"
-      | (id,_,t)::rest -> 
-	  (try let dir = faildir t gl in 
-	       general_rewrite dir (mkVar id) gl
-	   with Failure _ | UserError _  ->  arec rest)
-   in arec (pf_hyps gl)
-
-
-let rewrite_assumption_cond_in faildir hyp gl =
-   let rec arec = function
-      | [] -> error "No such assumption"
-      | (id,_,t)::rest -> 
-	  (try let dir = faildir t gl in 
-	       general_rewrite_in dir hyp (mkVar id) gl
-	   with Failure _ | UserError _ ->  arec rest)
-   in arec (pf_hyps gl)
-
 let cond_eq_term_left c t gl =
   try
     let (_,x,_) = snd (find_eq_data_decompose t) in
@@ -1189,6 +1170,48 @@ let cond_eq_term c t gl =
     else failwith "not convertible"
   with PatternMatchingFailure -> failwith "not an equality"
 
+let rewrite_mutli_assumption_cond cond_eq_term cl gl = 
+  let rec arec = function 
+    | [] -> error "No such assumption"
+    | (id,_,t) ::rest -> 
+	begin 
+	  try 
+	    let dir = cond_eq_term t gl in 
+	    general_multi_rewrite dir (mkVar id,NoBindings) cl gl
+	  with | Failure _ | UserError _ -> arec rest
+	end
+  in 
+  arec (pf_hyps gl)
+
+let replace_multi_term dir_opt c  = 
+  let cond_eq_fun = 
+    match dir_opt with 
+      | None -> cond_eq_term c
+      | Some true -> cond_eq_term_left c
+      | Some false -> cond_eq_term_right c
+  in 
+  rewrite_mutli_assumption_cond cond_eq_fun 
+
+(* JF. old version 
+let rewrite_assumption_cond faildir gl =
+   let rec arec = function
+      | [] -> error "No such assumption"
+      | (id,_,t)::rest ->
+	  (try let dir = faildir t gl in
+	       general_rewrite dir (mkVar id) gl
+	   with Failure _ | UserError _  ->  arec rest)
+   in arec (pf_hyps gl)
+
+
+let rewrite_assumption_cond_in faildir hyp gl =
+   let rec arec = function
+      | [] -> error "No such assumption"
+      | (id,_,t)::rest ->
+	  (try let dir = faildir t gl in
+	       general_rewrite_in dir hyp (mkVar id) gl
+	   with Failure _ | UserError _ ->  arec rest)
+   in arec (pf_hyps gl)
+
 let replace_term_left t = rewrite_assumption_cond (cond_eq_term_left t)
 
 let replace_term_right t = rewrite_assumption_cond (cond_eq_term_right t)
@@ -1200,6 +1223,27 @@ let replace_term_in_left t = rewrite_assumption_cond_in (cond_eq_term_left t)
 let replace_term_in_right t = rewrite_assumption_cond_in (cond_eq_term_right t)
    
 let replace_term_in t = rewrite_assumption_cond_in (cond_eq_term t)
+*)
+
+let replace_term_left t = replace_multi_term (Some true) t Tacticals.onConcl
+
+let replace_term_right t = replace_multi_term (Some false) t Tacticals.onConcl
+
+let replace_term t = replace_multi_term None t Tacticals.onConcl
+
+let replace_term_in_left t hyp = replace_multi_term (Some true) t (Tacticals.onHyp hyp)
+
+let replace_term_in_right t hyp = replace_multi_term (Some false) t (Tacticals.onHyp hyp)
+
+let replace_term_in t hyp = replace_multi_term None t (Tacticals.onHyp hyp)
+
+
+
+
+
+
+
+
 
-let _ = Setoid_replace.register_replace replace
+let _ = Setoid_replace.register_replace (fun tac_opt c2 c1 gl ->  replace_in_clause_maybe_by c2 c1 onConcl tac_opt gl)
 let _ = Setoid_replace.register_general_rewrite general_rewrite
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 12f9becbe8..ce38c7166b 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -50,11 +50,12 @@ val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic
 val conditional_rewrite_in :
   bool -> identifier -> tactic -> constr with_bindings -> tactic
 
+val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic
 val replace    : constr -> constr -> tactic
 val replace_in : identifier -> constr -> constr -> tactic
-val replace_by : constr -> constr -> tactic -> tactic 
-val replace_in_by : identifier -> constr -> constr -> tactic -> tactic 
-val new_replace : constr -> constr -> identifier option -> tactic option -> tactic
+val replace_by : constr -> constr -> tactic -> tactic
+val replace_in_by : identifier -> constr -> constr -> tactic -> tactic
+
 val discr        : identifier -> tactic
 val discrConcl   : tactic
 val discrClause  : clause -> tactic
@@ -111,9 +112,8 @@ val subst : identifier list -> tactic
 val subst_all : tactic
 
 (* Replace term *)
-val replace_term_left : constr -> tactic
-val replace_term_right : constr -> tactic
-val replace_term : constr -> tactic
-val replace_term_in_left : constr -> identifier -> tactic
-val replace_term_in_right : constr -> identifier -> tactic
-val replace_term_in : constr -> identifier -> tactic
+(* [replace_multi_term dir_opt c cl] 
+   perfoms replacement of [c] by the first value found in context
+   (according to [dir] if given to get the rewrite direction)  in the clause [cl]
+*)
+val replace_multi_term : bool option -> constr -> clause -> tactic
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 665a7bd752..a3580c3453 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -124,3 +124,125 @@ ARGUMENT EXTEND hloc
    
  END
 
+
+
+
+
+
+
+(* Julien: Mise en commun des differentes version de replace with in by *)
+
+let pr_by_arg_tac _prc _prlc prtac opt_c = 
+  match opt_c with 
+    | None -> mt ()
+    | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
+
+ARGUMENT EXTEND by_arg_tac
+  TYPED AS tactic_opt
+  PRINTED BY pr_by_arg_tac
+| [ "by" tactic3(c) ] -> [ Some c ]
+| [ ] -> [ None ]
+END
+ 
+
+let pr_in_hyp  pr_id (lo,concl) :  Pp.std_ppcmds = 
+  match lo,concl with 
+    | Some [],true -> mt ()
+    | None,true -> str "in" ++ spc () ++ str "*"
+    | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-" 
+    | Some l,_ -> 
+	str "in" ++ spc () ++ 
+	  Util.prlist_with_sep spc pr_id l ++ 
+	  match concl with 
+	    | true -> spc () ++ str "|-" ++ spc () ++ str "*"
+	    | _ -> mt ()
+
+
+let pr_in_arg_hyp _ _ _ = pr_in_hyp (fun (_,id) -> Ppconstr.pr_id id)
+
+let pr_in_arg_hyp_typed  _ _  _  = pr_in_hyp Ppconstr.pr_id 
+
+
+let pr_var_list_gen pr_id = Util.prlist_with_sep (fun () -> str ",") pr_id 
+
+let pr_var_list_typed _ _ _ =  pr_var_list_gen Ppconstr.pr_id 
+
+let pr_var_list _ _ _ = pr_var_list_gen (fun (_,id) -> Ppconstr.pr_id id)
+
+
+ARGUMENT EXTEND comma_var_lne 
+  TYPED AS var list 
+  PRINTED BY pr_var_list_typed
+  RAW_TYPED AS var list 
+  RAW_PRINTED BY pr_var_list
+  GLOB_TYPED AS var list
+  GLOB_PRINTED BY pr_var_list
+| [ var(x) ] -> [ [x] ]
+| [ var(x) "," comma_var_lne(l) ] -> [x::l]
+END
+
+ARGUMENT EXTEND comma_var_l 
+  TYPED AS var list 
+  PRINTED BY pr_var_list_typed
+  RAW_TYPED AS var list 
+  RAW_PRINTED BY pr_var_list
+  GLOB_TYPED AS var list
+  GLOB_PRINTED BY pr_var_list
+| [  comma_var_lne(l) ] -> [l]
+| [] -> [ [] ]
+END
+
+let pr_in_concl _ _ _ = function true -> str "|- " ++ spc () ++ str "*" | _ -> str "|-" 
+
+ARGUMENT EXTEND inconcl  
+  TYPED AS bool 
+  PRINTED BY pr_in_concl
+| [ "|-" "*" ] -> [ true ]
+| [ "|-" ] -> [ false ]
+END
+
+
+
+ARGUMENT EXTEND in_arg_hyp
+  TYPED AS var list option * bool
+  PRINTED BY pr_in_arg_hyp_typed
+  RAW_TYPED AS var list option * bool 
+  RAW_PRINTED BY pr_in_arg_hyp
+  GLOB_TYPED AS var list option * bool
+  GLOB_PRINTED BY pr_in_arg_hyp
+| [ "in" "*" ] -> [(None,true)]
+| [ "in" "*" inconcl_opt(b) ] -> [let onconcl = match b with Some b -> b | None -> true in (None,onconcl)]
+| [ "in" comma_var_l(l) inconcl_opt(b) ] -> [ let onconcl = match b with Some b -> b | None -> false in 
+					      Some l, onconcl
+					   ]
+| [ ] -> [ (Some [],true) ]
+END
+
+
+let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = 
+  {Tacexpr.onhyps=
+   Util.option_map 
+     (fun l -> 
+	List.map 
+	  (fun id -> ( ([],trad_id id) ,Tacexpr.InHyp))
+	  l
+     )
+     hyps;
+   Tacexpr.onconcl=concl;
+   Tacexpr.concl_occs = []}
+
+
+let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd 
+let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x) 
+
+
+let pr_term_dir _ _ _ = function | true -> str "->" | false -> str  "<-" 
+
+
+ARGUMENT EXTEND replace_term_dir 
+  TYPED AS bool 
+  PRINTED BY pr_term_dir 
+  | ["->"] -> [ true ]
+  | ["<-"] -> [ false ]
+END
+
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 6fcf728331..01da2dc110 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -20,117 +20,17 @@ open Names
 (* Equality *)
 open Equality
 
-(* Pierre L: for an easy implementation of "rewrite ... in <clause>", rewrite
-  has moved to g_tactics.ml4
-
-TACTIC EXTEND rewrite
-| [ "rewrite" orient(b) constr_with_bindings(c) ] ->
-    [general_rewrite_bindings b c]
-END
-
-TACTIC EXTEND rewrite_in
-| [ "rewrite" orient(b) constr_with_bindings(c) "in" hyp(h) ] ->
-    [general_rewrite_bindings_in b h c]
-END
-
-let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings) 
-*)
-
-(* Julien: Mise en commun des differentes version de replace with in by 
-   TODO: deplacer dans extraargs
-
-*)
-
-let pr_by_arg_tac _prc _prlc prtac opt_c = 
-  match opt_c with 
-    | None -> mt ()
-    | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
-
-let pr_in_hyp = function
-  | None -> mt ()
-  | Some id -> spc () ++ hov 2 (str "in" ++ spc () ++ Nameops.pr_id id)
-
-let pr_in_arg_hyp _prc _prlc _prtac opt_c =
-  pr_in_hyp (Util.option_map snd opt_c)
-
-let pr_in_arg_hyp_typed _prc _prlc _prtac =
-  pr_in_hyp
-
-ARGUMENT EXTEND by_arg_tac
-  TYPED AS tactic_opt
-  PRINTED BY pr_by_arg_tac
-| [ "by" tactic3(c) ] -> [ Some c ]
-| [ ] -> [ None ]
-END
- 
-ARGUMENT EXTEND in_arg_hyp
-  TYPED AS var_opt
-  PRINTED BY pr_in_arg_hyp_typed
-  RAW_TYPED AS var_opt
-  RAW_PRINTED BY pr_in_arg_hyp
-  GLOB_TYPED AS var_opt
-  GLOB_PRINTED BY pr_in_arg_hyp
-| [ "in" hyp(c) ] -> [ Some (c) ]
-| [ ] -> [ None ]
-END
 
 TACTIC EXTEND replace 
    ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ]
--> [ new_replace c1 c2 in_hyp (Util.option_map Tacinterp.eval_tactic tac) ]
+-> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Util.option_map Tacinterp.eval_tactic tac) ]
 END
 
-(* Julien:
-  old version  
-
-TACTIC EXTEND replace
-| [ "replace" constr(c1) "with" constr(c2) ] ->
-    [ replace c1 c2 ]
+TACTIC EXTEND replace_term 
+| [ "replace" replace_term_dir_opt(dir) constr(c) in_arg_hyp(in_hyp) ] -> 
+  [ replace_multi_term dir c (glob_in_arg_hyp_to_clause in_hyp)  ]
 END
 
-TACTIC EXTEND replace_by
-|  [ "replace" constr(c1) "with" constr(c2) "by" tactic(tac) ] ->
-    [ replace_by c1 c2 (snd tac)  ]
- 
-END
-
-TACTIC EXTEND replace_in
-| [ "replace" constr(c1) "with" constr(c2) "in" hyp(h) ] ->
-    [ replace_in h c1 c2 ]
-END
-
-TACTIC EXTEND replace_in_by
-| [ "replace" constr(c1) "with" constr(c2) "in" hyp(h) "by" tactic(tac) ] ->
-    [ replace_in_by h c1 c2 (snd tac) ]
-END
-
-*)
-
-TACTIC EXTEND replace_term_left
-  [ "replace" "->" constr(c)  ] -> [ replace_term_left c ]
-END
-
-TACTIC EXTEND replace_term_right
-  [ "replace" "<-" constr(c)  ] -> [ replace_term_right c ]
-END
-
-TACTIC EXTEND replace_term
-  [ "replace" constr(c)  ] -> [ replace_term c ]
-END
-
-TACTIC EXTEND replace_term_in_left
-  [ "replace"  "->" constr(c) "in" hyp(h) ]
-  -> [ replace_term_in_left c h ]
-END
-
-TACTIC EXTEND replace_term_in_right
-  [ "replace"  "<-" constr(c) "in" hyp(h) ]
-  -> [ replace_term_in_right c h ]
-END
-
-TACTIC EXTEND replace_term_in
-  [ "replace" constr(c) "in" hyp(h) ]
-  -> [ replace_term_in c h ]
-END
 
 TACTIC EXTEND simplify_eq
   [ "simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ]
@@ -182,7 +82,7 @@ END
 (* AutoRewrite *)
 
 open Autorewrite
-
+(* J.F : old version 
 TACTIC EXTEND autorewrite
   [ "autorewrite" "with" ne_preident_list(l) ] ->
     [ autorewrite Refiner.tclIDTAC l ]
@@ -193,6 +93,21 @@ TACTIC EXTEND autorewrite
 | [ "autorewrite" "with" ne_preident_list(l) "in" hyp(id) "using" tactic(t) ] ->
     [ autorewrite_in id (snd t) l ]
 END
+*)
+
+TACTIC EXTEND autorewrite
+| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) ] ->
+    [ auto_multi_rewrite  l (glob_in_arg_hyp_to_clause  cl) ]
+| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] ->
+    [ 
+      let cl =  glob_in_arg_hyp_to_clause cl in 
+      auto_multi_rewrite_with (snd t) l cl
+
+    ]
+END
+
+
+
 
 let add_rewrite_hint name ort t lcsr =
   let env = Global.env() and sigma = Evd.empty in
@@ -223,22 +138,22 @@ let refine_tac = h_refine
 open Setoid_replace
 
 TACTIC EXTEND setoid_replace
-   [ "setoid_replace" constr(c1) "with" constr(c2) ] ->
-     [ setoid_replace None c1 c2 ~new_goals:[] ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel)] ->
-     [ setoid_replace (Some rel) c1 c2 ~new_goals:[] ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) ] ->
-     [ 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 ]
+   [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] ->
+     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] ->
+     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] ->
+     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] ->
+     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] ->
+     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] ->
+     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] ->
+     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) 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) by_arg_tac(tac)] ->
+     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ]
 END
 
 TACTIC EXTEND setoid_rewrite
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index ce9bff52cc..23d4a275d1 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -22,21 +22,3 @@ val h_injHyp : quantified_hypothesis -> tactic
 
 val refine_tac : Genarg.open_constr -> tactic
 
-
-
-(* Julien: Mise en commun des differentes version de replace with in by 
-   TODO:  deplacer dans extraargs
-
-*)
-
-
-val rawwit_in_arg_hyp: identifier located option raw_abstract_argument_type
-
-val in_arg_hyp: identifier located option Pcoq.Gram.Entry.e
-
-
-
-val rawwit_by_arg_tac :
-  (raw_tactic_expr option, constr_expr, raw_tactic_expr) abstract_argument_type
-  
-val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index e990255370..e9a204ada5 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -33,7 +33,7 @@ open Decl_kinds
 open Constrintern
 open Mod_subst
 
-let replace = ref (fun _ _ -> assert false)
+let replace = ref (fun _ _ _ -> assert false)
 let register_replace f = replace := f
 
 let general_rewrite = ref (fun _ _ -> assert false)
@@ -1849,8 +1849,27 @@ let general_s_rewrite_in id lft2rgt c ~new_goals gl =
   else 
     relation_rewrite_in id c2 c1 (Right2Left,eqclause) ~new_goals gl
 
-let setoid_replace relation c1 c2 ~new_goals gl =
- try
+
+(* 
+   [general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals ]
+   common part of [setoid_replace] and [setoid_replace_in]  (distinction is done using rewrite_tac). 
+
+   Algorith sketch: 
+   1- find the (setoid) relation [rel] between [c1] and [c2] using [relation]
+   2- assert [H:rel c2 c1] 
+   3- replace [c1] with [c2] using [rewrite_tac] (should be [general_s_rewrite] if we want to replace in the 
+      goal, and [general_s_rewrite_in id] if we want to replace in the hypothesis [id]). Possibly generate
+      new_goals if asked (cf general_s_rewrite)
+   4- if [try_prove_eq_tac_opt] is [Some tac] try to complete [rel c2 c1] using tac and do nothing if 
+      [try_prove_eq_tac_opt] is [None]
+*)
+let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals gl =
+  let try_prove_eq_tac = 
+    match try_prove_eq_tac_opt with 
+      | None -> Tacticals.tclIDTAC
+      | Some tac ->  Tacticals.tclTRY (Tacticals.tclCOMPLETE tac )
+  in 
+  try
   let relation =
    match relation with
       Some rel ->
@@ -1873,23 +1892,29 @@ let setoid_replace relation c1 c2 ~new_goals gl =
     tclTHENS (assert_tac false Anonymous eq)
       [onLastHyp (fun id ->
         tclTHEN
-          (general_s_rewrite dir (mkVar id) ~new_goals)
+          (rewrite_tac dir (mkVar id) ~new_goals)
           (clear [id]));
-       Tacticals.tclIDTAC]
+       try_prove_eq_tac]
    in
     tclORELSE
      (replace true eq_left_to_right) (replace false eq_right_to_left) gl
  with
-  Optimize -> (!replace c1 c2) gl
+  Optimize -> (* (!replace tac_opt c1 c2) gl *)
+    let eq =  mkApp (Lazy.force  coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in 
+    tclTHENS (assert_tac false Anonymous eq)
+      [onLastHyp (fun id ->
+		    tclTHEN
+		      (rewrite_tac false (mkVar id) ~new_goals)
+		      (clear [id]));
+       try_prove_eq_tac] 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
- cut_replacing id new_hyp
-   (fun exact -> tclTHENLASTn
-     (setoid_replace relation c2 c1 ~new_goals)
-     [| exact; tclIDTAC |]) gl
 
+let setoid_replace = general_setoid_replace general_s_rewrite
+let setoid_replace_in  tac_opt id relation c1 c2 ~new_goals gl = 
+  general_setoid_replace (general_s_rewrite_in id)  tac_opt relation c1 c2 ~new_goals gl
+ 
 (* [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
 let setoid_reflexivity gl =
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index b8bed63c54..ecad6a574e 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -39,7 +39,7 @@ type morphism_signature = (bool option * constr_expr) list * constr_expr
 
 val pr_morphism_signature : morphism_signature -> Pp.std_ppcmds
 
-val register_replace : (constr -> constr -> tactic) -> unit
+val register_replace : (tactic option -> constr -> constr -> tactic) -> unit
 val register_general_rewrite : (bool -> constr -> tactic) -> unit
 
 val print_setoids : unit -> unit
@@ -52,8 +52,9 @@ val default_morphism :
   ?filter:(constr morphism -> bool) -> constr -> relation morphism
 
 val setoid_replace :
- constr option -> constr -> constr -> new_goals:constr list -> tactic
+  tactic option -> constr option -> constr -> constr -> new_goals:constr list -> tactic
 val setoid_replace_in :
+  tactic option -> 
  identifier -> constr option -> constr -> constr -> new_goals:constr list ->
   tactic