+ 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

18 files changed, 589 insertions, 347 deletions

diff --git a/.depend b/.depend
index 04f8de6dbf..46b3ece083 100644
--- a/.depend
+++ b/.depend
@@ -262,8 +262,8 @@ tactics/auto.cmi: toplevel/vernacexpr.cmo lib/util.cmi kernel/term.cmi \
     pretyping/pattern.cmi kernel/names.cmi kernel/mod_subst.cmi \
     library/libnames.cmi pretyping/evd.cmi kernel/environ.cmi \
     pretyping/clenv.cmi tactics/btermdn.cmi 
-tactics/autorewrite.cmi: kernel/term.cmi proofs/tacmach.cmi \
-    proofs/tacexpr.cmo kernel/names.cmi 
+tactics/autorewrite.cmi: kernel/term.cmi tactics/tacticals.cmi \
+    proofs/tacmach.cmi proofs/tacexpr.cmo kernel/names.cmi 
 tactics/btermdn.cmi: kernel/term.cmi pretyping/pattern.cmi 
 tactics/contradiction.cmi: kernel/term.cmi pretyping/rawterm.cmi \
     proofs/proof_type.cmi kernel/names.cmi 
@@ -282,11 +282,12 @@ tactics/equality.cmi: kernel/term.cmi tactics/tactics.cmi \
 tactics/evar_tactics.cmi: kernel/term.cmi proofs/tacmach.cmi \
     proofs/tacexpr.cmo pretyping/rawterm.cmi kernel/names.cmi 
 tactics/extraargs.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \
-    proofs/tacexpr.cmo tactics/setoid_replace.cmi pretyping/rawterm.cmi \
-    proofs/proof_type.cmi parsing/pcoq.cmi kernel/names.cmi 
+    tactics/tacticals.cmi proofs/tacexpr.cmo tactics/setoid_replace.cmi \
+    pretyping/rawterm.cmi proofs/proof_type.cmi parsing/pcoq.cmi \
+    kernel/names.cmi 
 tactics/extratactics.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \
     proofs/tacexpr.cmo pretyping/rawterm.cmi proofs/proof_type.cmi \
-    parsing/pcoq.cmi kernel/names.cmi interp/genarg.cmi 
+    kernel/names.cmi interp/genarg.cmi 
 tactics/hiddentac.cmi: kernel/term.cmi tactics/tacticals.cmi \
     proofs/tacmach.cmi proofs/tacexpr.cmo proofs/redexpr.cmi \
     pretyping/rawterm.cmi proofs/proof_type.cmi kernel/names.cmi \
@@ -1725,19 +1726,21 @@ tactics/auto.cmx: toplevel/vernacexpr.cmx lib/util.cmx pretyping/typing.cmx \
 tactics/autorewrite.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/typing.cmi kernel/term.cmi tactics/tactics.cmi \
     tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \
-    proofs/tacexpr.cmo library/summary.cmi proofs/proof_type.cmi \
-    parsing/printer.cmi parsing/pptactic.cmi lib/pp.cmi kernel/names.cmi \
-    kernel/mod_subst.cmi library/libobject.cmi library/lib.cmi \
-    tactics/hipattern.cmi library/global.cmi pretyping/evd.cmi \
-    tactics/equality.cmi kernel/environ.cmi tactics/autorewrite.cmi 
+    proofs/tacexpr.cmo library/summary.cmi proofs/refiner.cmi \
+    proofs/proof_type.cmi parsing/printer.cmi parsing/pptactic.cmi lib/pp.cmi \
+    kernel/names.cmi kernel/mod_subst.cmi library/libobject.cmi \
+    library/lib.cmi tactics/hipattern.cmi library/global.cmi \
+    pretyping/evd.cmi tactics/equality.cmi kernel/environ.cmi \
+    tactics/autorewrite.cmi 
 tactics/autorewrite.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     pretyping/typing.cmx kernel/term.cmx tactics/tactics.cmx \
     tactics/tacticals.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \
-    proofs/tacexpr.cmx library/summary.cmx proofs/proof_type.cmx \
-    parsing/printer.cmx parsing/pptactic.cmx lib/pp.cmx kernel/names.cmx \
-    kernel/mod_subst.cmx library/libobject.cmx library/lib.cmx \
-    tactics/hipattern.cmx library/global.cmx pretyping/evd.cmx \
-    tactics/equality.cmx kernel/environ.cmx tactics/autorewrite.cmi 
+    proofs/tacexpr.cmx library/summary.cmx proofs/refiner.cmx \
+    proofs/proof_type.cmx parsing/printer.cmx parsing/pptactic.cmx lib/pp.cmx \
+    kernel/names.cmx kernel/mod_subst.cmx library/libobject.cmx \
+    library/lib.cmx tactics/hipattern.cmx library/global.cmx \
+    pretyping/evd.cmx tactics/equality.cmx kernel/environ.cmx \
+    tactics/autorewrite.cmi 
 tactics/btermdn.cmo: tactics/termdn.cmi kernel/term.cmi pretyping/pattern.cmi \
     library/libnames.cmi tactics/dn.cmi tactics/btermdn.cmi 
 tactics/btermdn.cmx: tactics/termdn.cmx kernel/term.cmx pretyping/pattern.cmx \
@@ -1860,24 +1863,25 @@ tactics/evar_tactics.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
     proofs/refiner.cmx proofs/proof_type.cmx pretyping/evd.cmx \
     pretyping/evarutil.cmx proofs/evar_refiner.cmx kernel/environ.cmx \
     tactics/evar_tactics.cmi 
-tactics/extraargs.cmo: lib/util.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
-    tactics/setoid_replace.cmi parsing/printer.cmi parsing/pptactic.cmi \
-    lib/pp.cmi parsing/pcoq.cmi kernel/names.cmi library/nameops.cmi \
-    toplevel/metasyntax.cmi parsing/lexer.cmi interp/genarg.cmi \
-    tactics/extraargs.cmi 
-tactics/extraargs.cmx: lib/util.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
-    tactics/setoid_replace.cmx parsing/printer.cmx parsing/pptactic.cmx \
-    lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx library/nameops.cmx \
-    toplevel/metasyntax.cmx parsing/lexer.cmx interp/genarg.cmx \
-    tactics/extraargs.cmi 
+tactics/extraargs.cmo: lib/util.cmi tactics/tacticals.cmi \
+    tactics/tacinterp.cmi proofs/tacexpr.cmo tactics/setoid_replace.cmi \
+    parsing/printer.cmi parsing/pptactic.cmi interp/ppextend.cmi \
+    parsing/ppconstr.cmi lib/pp.cmi parsing/pcoq.cmi kernel/names.cmi \
+    library/nameops.cmi toplevel/metasyntax.cmi parsing/lexer.cmi \
+    interp/genarg.cmi tactics/extraargs.cmi 
+tactics/extraargs.cmx: lib/util.cmx tactics/tacticals.cmx \
+    tactics/tacinterp.cmx proofs/tacexpr.cmx tactics/setoid_replace.cmx \
+    parsing/printer.cmx parsing/pptactic.cmx interp/ppextend.cmx \
+    parsing/ppconstr.cmx lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx \
+    library/nameops.cmx toplevel/metasyntax.cmx parsing/lexer.cmx \
+    interp/genarg.cmx tactics/extraargs.cmi 
 tactics/extratactics.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
     tactics/tacinterp.cmi proofs/tacexpr.cmo library/summary.cmi \
     tactics/setoid_replace.cmi proofs/refiner.cmi tactics/refine.cmi \
-    pretyping/rawterm.cmi parsing/pptactic.cmi interp/ppextend.cmi lib/pp.cmi \
-    parsing/pcoq.cmi kernel/names.cmi library/nameops.cmi \
-    kernel/mod_subst.cmi library/libobject.cmi library/libnames.cmi \
-    library/lib.cmi parsing/lexer.cmi tactics/leminv.cmi tactics/inv.cmi \
+    pretyping/rawterm.cmi parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi \
+    kernel/names.cmi kernel/mod_subst.cmi library/libobject.cmi \
+    library/libnames.cmi library/lib.cmi tactics/leminv.cmi tactics/inv.cmi \
     library/global.cmi interp/genarg.cmi tactics/extraargs.cmi \
     pretyping/evd.cmi tactics/evar_tactics.cmi tactics/equality.cmi \
     parsing/egrammar.cmi tactics/contradiction.cmi interp/constrintern.cmi \
@@ -1886,10 +1890,9 @@ tactics/extratactics.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \
     tactics/tacinterp.cmx proofs/tacexpr.cmx library/summary.cmx \
     tactics/setoid_replace.cmx proofs/refiner.cmx tactics/refine.cmx \
-    pretyping/rawterm.cmx parsing/pptactic.cmx interp/ppextend.cmx lib/pp.cmx \
-    parsing/pcoq.cmx kernel/names.cmx library/nameops.cmx \
-    kernel/mod_subst.cmx library/libobject.cmx library/libnames.cmx \
-    library/lib.cmx parsing/lexer.cmx tactics/leminv.cmx tactics/inv.cmx \
+    pretyping/rawterm.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \
+    kernel/names.cmx kernel/mod_subst.cmx library/libobject.cmx \
+    library/libnames.cmx library/lib.cmx tactics/leminv.cmx tactics/inv.cmx \
     library/global.cmx interp/genarg.cmx tactics/extraargs.cmx \
     pretyping/evd.cmx tactics/evar_tactics.cmx tactics/equality.cmx \
     parsing/egrammar.cmx tactics/contradiction.cmx interp/constrintern.cmx \
@@ -2068,9 +2071,9 @@ tactics/tacticals.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
     pretyping/evd.cmx proofs/evar_refiner.cmx kernel/environ.cmx \
     kernel/declarations.cmx proofs/clenvtac.cmx pretyping/clenv.cmx \
     tactics/tacticals.cmi 
-tactics/tactics.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
-    tactics/tacticals.cmi pretyping/tacred.cmi proofs/tacmach.cmi \
-    proofs/tacexpr.cmo kernel/sign.cmi proofs/refiner.cmi \
+tactics/tactics.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \
+    kernel/term.cmi tactics/tacticals.cmi pretyping/tacred.cmi \
+    proofs/tacmach.cmi proofs/tacexpr.cmo kernel/sign.cmi proofs/refiner.cmi \
     pretyping/reductionops.cmi kernel/reduction.cmi proofs/redexpr.cmi \
     pretyping/rawterm.cmi proofs/proof_type.cmi proofs/proof_trees.cmi \
     pretyping/pretype_errors.cmi lib/pp.cmi proofs/pfedit.cmi lib/options.cmi \
@@ -2082,9 +2085,9 @@ tactics/tactics.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
     library/declare.cmi kernel/declarations.cmi library/decl_kinds.cmo \
     interp/coqlib.cmi interp/constrintern.cmi proofs/clenvtac.cmi \
     pretyping/clenv.cmi tactics/tactics.cmi 
-tactics/tactics.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
-    tactics/tacticals.cmx pretyping/tacred.cmx proofs/tacmach.cmx \
-    proofs/tacexpr.cmx kernel/sign.cmx proofs/refiner.cmx \
+tactics/tactics.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \
+    kernel/term.cmx tactics/tacticals.cmx pretyping/tacred.cmx \
+    proofs/tacmach.cmx proofs/tacexpr.cmx kernel/sign.cmx proofs/refiner.cmx \
     pretyping/reductionops.cmx kernel/reduction.cmx proofs/redexpr.cmx \
     pretyping/rawterm.cmx proofs/proof_type.cmx proofs/proof_trees.cmx \
     pretyping/pretype_errors.cmx lib/pp.cmx proofs/pfedit.cmx lib/options.cmx \
@@ -2936,26 +2939,28 @@ contrib/funind/indfun_common.cmx: lib/util.cmx pretyping/termops.cmx \
     contrib/funind/indfun_common.cmi 
 contrib/funind/indfun_main.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \
-    tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \
-    proofs/tacexpr.cmo proofs/refiner.cmi pretyping/rawterm.cmi \
-    proofs/proof_type.cmi parsing/printer.cmi parsing/pptactic.cmi \
-    parsing/ppconstr.cmi lib/pp.cmi parsing/pcoq.cmi library/nametab.cmi \
-    kernel/names.cmi library/nameops.cmi parsing/lexer.cmi \
-    contrib/funind/invfun.cmo contrib/funind/indfun_common.cmi \
-    contrib/funind/indfun.cmo interp/genarg.cmi \
+    tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \
+    tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/refiner.cmi \
+    pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \
+    parsing/pptactic.cmi parsing/ppconstr.cmi lib/pp.cmi parsing/pcoq.cmi \
+    library/nametab.cmi kernel/names.cmi library/nameops.cmi \
+    parsing/lexer.cmi contrib/funind/invfun.cmo \
+    contrib/funind/indfun_common.cmi contrib/funind/indfun.cmo \
+    library/global.cmi interp/genarg.cmi \
     contrib/funind/functional_principles_types.cmi parsing/egrammar.cmi \
-    toplevel/cerrors.cmi 
+    interp/coqlib.cmi toplevel/cerrors.cmi 
 contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \
-    tactics/tacticals.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \
-    proofs/tacexpr.cmx proofs/refiner.cmx pretyping/rawterm.cmx \
-    proofs/proof_type.cmx parsing/printer.cmx parsing/pptactic.cmx \
-    parsing/ppconstr.cmx lib/pp.cmx parsing/pcoq.cmx library/nametab.cmx \
-    kernel/names.cmx library/nameops.cmx parsing/lexer.cmx \
-    contrib/funind/invfun.cmx contrib/funind/indfun_common.cmx \
-    contrib/funind/indfun.cmx interp/genarg.cmx \
+    tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \
+    tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/refiner.cmx \
+    pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \
+    parsing/pptactic.cmx parsing/ppconstr.cmx lib/pp.cmx parsing/pcoq.cmx \
+    library/nametab.cmx kernel/names.cmx library/nameops.cmx \
+    parsing/lexer.cmx contrib/funind/invfun.cmx \
+    contrib/funind/indfun_common.cmx contrib/funind/indfun.cmx \
+    library/global.cmx interp/genarg.cmx \
     contrib/funind/functional_principles_types.cmx parsing/egrammar.cmx \
-    toplevel/cerrors.cmx 
+    interp/coqlib.cmx toplevel/cerrors.cmx 
 contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \
     tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \
@@ -3016,16 +3021,16 @@ contrib/funind/invfun.cmx: toplevel/vernacentries.cmx lib/util.cmx \
     kernel/entries.cmx kernel/declarations.cmx library/decl_kinds.cmx \
     interp/coqlib.cmx toplevel/command.cmx kernel/closure.cmx \
     toplevel/cerrors.cmx 
-contrib/funind/rawtermops.cmo: lib/util.cmi pretyping/rawterm.cmi \
-    parsing/printer.cmi parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi \
-    library/nameops.cmi library/libnames.cmi pretyping/inductiveops.cmi \
-    contrib/funind/indfun_common.cmi library/global.cmi pretyping/evd.cmi \
-    interp/coqlib.cmi contrib/funind/rawtermops.cmi 
-contrib/funind/rawtermops.cmx: lib/util.cmx pretyping/rawterm.cmx \
-    parsing/printer.cmx parsing/ppconstr.cmx lib/pp.cmx kernel/names.cmx \
-    library/nameops.cmx library/libnames.cmx pretyping/inductiveops.cmx \
-    contrib/funind/indfun_common.cmx library/global.cmx pretyping/evd.cmx \
-    interp/coqlib.cmx contrib/funind/rawtermops.cmi 
+contrib/funind/rawtermops.cmo: lib/util.cmi pretyping/rawterm.cmi lib/pp.cmi \
+    kernel/names.cmi library/nameops.cmi library/libnames.cmi \
+    pretyping/inductiveops.cmi contrib/funind/indfun_common.cmi \
+    library/global.cmi pretyping/evd.cmi interp/coqlib.cmi \
+    contrib/funind/rawtermops.cmi 
+contrib/funind/rawtermops.cmx: lib/util.cmx pretyping/rawterm.cmx lib/pp.cmx \
+    kernel/names.cmx library/nameops.cmx library/libnames.cmx \
+    pretyping/inductiveops.cmx contrib/funind/indfun_common.cmx \
+    library/global.cmx pretyping/evd.cmx interp/coqlib.cmx \
+    contrib/funind/rawtermops.cmi 
 contrib/funind/rawterm_to_relation.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     pretyping/typing.cmi interp/topconstr.cmi pretyping/termops.cmi \
     kernel/term.cmi tactics/tacinterp.cmi lib/system.cmi kernel/sign.cmi \
@@ -3298,18 +3303,16 @@ contrib/interface/xlate.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     interp/topconstr.cmi kernel/term.cmi proofs/tacexpr.cmo \
     pretyping/rawterm.cmi parsing/ppconstr.cmi parsing/pcoq.cmi \
     kernel/names.cmi library/libnames.cmi library/goptions.cmi \
-    interp/genarg.cmi contrib/field/field.cmo tactics/extratactics.cmi \
-    tactics/extraargs.cmi parsing/extend.cmi tactics/eauto.cmi \
-    library/decl_kinds.cmo lib/bigint.cmi contrib/interface/ascent.cmi \
-    contrib/interface/xlate.cmi 
+    interp/genarg.cmi contrib/field/field.cmo tactics/extraargs.cmi \
+    parsing/extend.cmi tactics/eauto.cmi library/decl_kinds.cmo \
+    lib/bigint.cmi contrib/interface/ascent.cmi contrib/interface/xlate.cmi 
 contrib/interface/xlate.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     interp/topconstr.cmx kernel/term.cmx proofs/tacexpr.cmx \
     pretyping/rawterm.cmx parsing/ppconstr.cmx parsing/pcoq.cmx \
     kernel/names.cmx library/libnames.cmx library/goptions.cmx \
-    interp/genarg.cmx contrib/field/field.cmx tactics/extratactics.cmx \
-    tactics/extraargs.cmx parsing/extend.cmx tactics/eauto.cmx \
-    library/decl_kinds.cmx lib/bigint.cmx contrib/interface/ascent.cmi \
-    contrib/interface/xlate.cmi 
+    interp/genarg.cmx contrib/field/field.cmx tactics/extraargs.cmx \
+    parsing/extend.cmx tactics/eauto.cmx library/decl_kinds.cmx \
+    lib/bigint.cmx contrib/interface/ascent.cmi contrib/interface/xlate.cmi 
 contrib/jprover/jall.cmo: lib/pp.cmi contrib/jprover/opname.cmi \
     contrib/jprover/jtunify.cmi contrib/jprover/jterm.cmi \
     contrib/jprover/jlogic.cmi contrib/jprover/jall.cmi 
@@ -4007,72 +4010,94 @@ tools/coq-tex.cmx:
 coq_fix_code.o: kernel/byterun/coq_fix_code.c \
   /usr/local/lib/ocaml/caml/config.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \
-  /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_fix_code.h
+  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/memory.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
 coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
   kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h \
+  /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
   kernel/byterun/coq_jumptbl.h
 coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
   kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h \
+  /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h
 coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/fail.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
   /usr/local/lib/ocaml/caml/alloc.h
 coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \
   /usr/local/lib/ocaml/caml/config.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \
-  /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_fix_code.h
+  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/memory.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
 coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
   kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h \
+  /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
   kernel/byterun/coq_jumptbl.h
 coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
-  /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
   kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
-  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/fail.h \
+  /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h
 coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
   /usr/local/lib/ocaml/caml/mlvalues.h \
   /usr/local/lib/ocaml/caml/compatibility.h \
-  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \
-  /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/fail.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/misc.h \
   /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
   /usr/local/lib/ocaml/caml/alloc.h
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 8f880a767e..97dfbfb1ed 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -21,7 +21,7 @@ and ct_BINDING =
     CT_binding of ct_ID_OR_INT * ct_FORMULA
 and ct_BINDING_LIST =
     CT_binding_list of ct_BINDING list
-and ct_BOOL =
+and t_BOOL =
     CT_false
   | CT_true
 and ct_CASE =
@@ -684,7 +684,7 @@ and ct_TACTIC_COM =
   | CT_reflexivity
   | CT_rename of ct_ID * ct_ID
   | CT_repeat of ct_TACTIC_COM
-  | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_ID_OPT * ct_TACTIC_OPT
+  | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_CLAUSE * ct_TACTIC_OPT
   | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE
   | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE
   | CT_right of ct_SPEC_LIST
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 064d20abd4..9c26c07111 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1711,7 +1711,7 @@ and fTACTIC_COM = function
 | CT_replace_with(x1, x2,x3,x4) ->
    fFORMULA x1;
    fFORMULA x2;
-   fID_OPT x3;
+   fCLAUSE x3;
    fTACTIC_OPT x4;
    fNODE "replace_with" 4
 | CT_rewrite_lr(x1, x2, x3) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 024cb59919..f2385e7f23 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -497,6 +497,8 @@ let xlate_hyp_location =
   | (_, MetaId _),_ -> 
       xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)"
 
+
+
 let xlate_clause cls =
   let hyps_info =
     match cls.onhyps with
@@ -972,22 +974,36 @@ and xlate_tac =
     | TacRight bindl -> CT_right (xlate_bindings bindl)
     | TacSplit (false,bindl) -> CT_split (xlate_bindings bindl)
     | TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl)
-    | TacExtend (_,"replace", [c1; c2;id_opt;tac_opt]) ->
+    | TacExtend (_,"replace", [c1; c2;cl;tac_opt]) ->
 	let c1 = xlate_formula (out_gen rawwit_constr c1) in
 	let c2 = xlate_formula (out_gen rawwit_constr c2) in
-	let id_opt = 
-	  match out_gen Extratactics.rawwit_in_arg_hyp id_opt with 
-	  | None -> ctv_ID_OPT_NONE
-	  | Some (_,id) ->   ctf_ID_OPT_SOME (xlate_ident id)
-	in
+	let cl = 
+	  (* J.F. : 18/08/2006 
+	     Hack to coerce the "clause" argument of replace to a real clause 
+	     To be remove if we can reuse the clause grammar entrie defined in g_tactic
+	  *)
+	  let cl_as_clause = Extraargs.raw_in_arg_hyp_to_clause (out_gen Extraargs.rawwit_in_arg_hyp cl) in 
+	  let cl_as_xlate_arg = 
+	    {cl_as_clause with 
+	       Tacexpr.onhyps = 
+		option_map 
+		  (fun l -> 
+		     List.map (fun ((l,id),hyp_flag) -> ((l, Tacexpr.AI ((),id)) ,hyp_flag)) l
+		  )
+		  cl_as_clause.Tacexpr.onhyps
+	    }
+	  in
+	  cl_as_xlate_arg
+	in 
+	let cl = xlate_clause cl in 
 	let tac_opt = 
-	  match out_gen (Extratactics.rawwit_by_arg_tac) tac_opt with
+	  match out_gen (Extraargs.rawwit_by_arg_tac) tac_opt with
 	    | None -> CT_coerce_NONE_to_TACTIC_OPT  CT_none
 	    | Some tac ->
 		let tac =  xlate_tactic tac in
 		CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
 	in 
-	CT_replace_with (c1, c2,id_opt,tac_opt)
+	CT_replace_with (c1, c2,cl,tac_opt)
     | TacRewrite(b,cbindl,cl) -> 
      let cl = xlate_clause cl 
      and c = xlate_formula (fst cbindl) 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 2421931626..1dd534ca29 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -725,11 +725,12 @@ can be either the conclusion, or an hypothesis. In the case of a
 defined hypothesis it is possible to specify if the conversion should
 occur on the type part, the body part or both (default).
 
-\index{Clauses}
-Clauses are written after a conversion tactic (tactic
-\texttt{set}~\ref{tactic:set} also uses clauses) and are introduced by
-the keyword \texttt{in}. If no clause is provided, the default is to
-perform the conversion only in the conclusion.
+\index{Clauses} Clauses are written after a conversion tactic (tactics
+\texttt{set}~\ref{tactic:set},          \texttt{rewrite}~\ref{rewrite},
+\texttt{replace}~\ref{tactic:replace}                               and
+\texttt{autorewrite}~\ref{tactic:autorewrite}  also  use clauses)  and
+are introduced by  the keyword \texttt{in}. If no  clause is provided,
+the default is to perform the conversion only in the conclusion.
 
 The syntax and description of the various clauses follows:
 \begin{description}
@@ -1603,6 +1604,7 @@ This tactic acts like {\tt replace {\term$_1$} with {\term$_2$}}
 (see below).
 
 \subsection{\tt replace {\term$_1$} with {\term$_2$}
+\label{tactic:replace}
 \tacindex{replace \dots\ with}}
 
 This tactic applies to any goal. It replaces all free occurrences of
@@ -1618,21 +1620,23 @@ n}| assumption || symmetry; try assumption]}.
 \end{ErrMsgs}
 
 \begin{Variants}
-  
-\item {\tt replace {\term$_1$} with {\term$_2$} in \ident}\\
-  This replaces {\term$_1$} with {\term$_2$} in the hypothesis named
-  {\ident}, and generates the subgoal {\term$_2$}{\tt =}{\term$_1$}. 
-
-%   \begin{ErrMsgs}
-%   \item \errindex{No such hypothesis} : {\ident}
-%   \item \errindex{Nothing to rewrite in {\ident}}
-%   \end{ErrMsgs}
-
-\item {\tt replace {\term$_1$} with  {\term$_2$} by \tac}\\ This acts as
-  {\tt  replace {\term$_1$}  with {\term$_2$}}  but try  to  solve the
+\item {\tt replace {\term$_1$} with {\term$_2$} by \tac}\\ This acts
+  as {\tt replace {\term$_1$} with {\term$_2$}} but try to solve the
   generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}.
-\item {\tt replace {\term$_1$} with {\term$_2$} in \ident by \tac}\\
-  This acts as {\tt replace {\term$_1$} with {\term$_2$} in \ident} but try to solve the generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}.
+\item {\tt replace {\term}}\\ Replace {\term} with {\term'} using the
+  first assumption which type has the form {\tt \term=\term'} or {\tt
+    \term'=\term}
+\item {\tt replace -> {\term}}\\ Replace {\term} with {\term'} using the
+  first assumption which type has the form {\tt \term=\term'}
+\item {\tt replace <- {\term}}\\ Replace {\term} with {\term'} using the
+  first assumption which type has the form {\tt \term'=\term}
+\item {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} }\\
+    {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} by \tac }\\ 
+    {\tt replace {\term} \textit{clause}}\\ 
+    {\tt replace -> {\term} \textit{clause}}\\ 
+    {\tt replace -> {\term} \textit{clause}}\\ 
+    Act as before but the replacements take place in \textit{clause}~\ref{Conversion-tactics} an not only in the conclusion of the goal.\\
+    The  \textit{clause} arg must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
 \end{Variants}
 
 \subsection{\tt reflexivity
@@ -2780,6 +2784,7 @@ Reset Initial.
 \end{coq_eval}
 
 \subsection{\tt autorewrite with \ident$_1$ \dots \ident$_n$.
+\label{tactic:autorewrite}
 \tacindex{autorewrite}}
 
 This tactic \footnote{The behavior of this tactic has much changed compared to
@@ -2806,9 +2811,17 @@ command.
 Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$
 $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
 
-\item \texttt{autorewrite with {\ident} in {\qualid}}
+\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}}
 
   Performs all the rewritings in hypothesis {\qualid}.
+\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}}
+
+  Performs all  the rewritings  in hypothesis {\qualid}  applying {\tt
+    \tac} to the main subgoal after each rewriting step.
+
+\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in \textit{clause}}
+  Performs all  the rewritings  in the clause \textit{clause}. \\
+  The  \textit{clause} arg must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
 
 \end{Variant}
 
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 10cd5b3ec6..030400e5cd 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -493,12 +493,14 @@ unprefixed form.
   ~\zeroone{\texttt{using relation} \textit{term}}\\
   ~\zeroone{\texttt{generate side conditions}
   \textit{term}$_1$ \ldots \textit{term}$_n$}\\
+  ~\zeroone{\texttt{by} \textit{tactic}}
 \end{verse}
 
-The \texttt{generate side conditions} and \texttt{using relation} arguments cannot be
-passed to the unprefixed form. The latter argument tells the tactic what
-parametric relation should be used to replace the first tactic argument
-with the second one. If omitted, it defaults to Leibniz equality.
+The  \texttt{generate  side  conditions} and  \texttt{using  relation}
+arguments cannot be passed to the unprefixed form. The latter argument
+tells the  tactic what parametric  relation should be used  to replace
+the first tactic argument with the second one. If omitted, it defaults
+to Leibniz equality.
 
 Every derived tactic that is based on the unprefixed forms of the tactics
 considered above will also work up to user defined relations. For instance,
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
 
diff --git a/test-suite/failure/autorewritein.v b/test-suite/failure/autorewritein.v
new file mode 100644
index 0000000000..dc17742a7d
--- /dev/null
+++ b/test-suite/failure/autorewritein.v
@@ -0,0 +1,15 @@
+Variable Ack : nat -> nat -> nat.
+
+Axiom Ack0 : forall m : nat, Ack 0 m = S m.
+Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1.
+Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
+
+Hint Rewrite Ack0 Ack1 Ack2 : base0.
+
+Lemma ResAck2 : forall H:(Ack 2 2 = 7 -> False), H=H  -> False.
+Proof.
+  intros.
+  autorewrite with base0 in * using try (apply H1;reflexivity).
+
+
+
diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewritein.v
index 8126e9e4ba..2f7d86dae1 100644
--- a/test-suite/success/autorewritein.v
+++ b/test-suite/success/autorewritein.v
@@ -18,3 +18,12 @@ Proof.
   autorewrite with base0 in H using try (apply H1; reflexivity).
 Qed.
 
+Lemma ResAck2 : forall H:(Ack 2 2 = 7 -> False), H=H  -> False.
+Proof.
+  intros.
+  autorewrite with base0 in *;
+    apply H1;reflexivity.
+Qed.
+
+
+
diff --git a/test-suite/success/replace.v b/test-suite/success/replace.v
new file mode 100644
index 0000000000..94b75c7f0f
--- /dev/null
+++ b/test-suite/success/replace.v
@@ -0,0 +1,24 @@
+Goal forall x, x = 0 -> S x = 7 -> x = 22 .
+Proof.
+replace 0 with 33.
+Undo.
+intros x H H0.
+replace x with 0.
+Undo.
+replace x with 0 in  |- *. 
+Undo.
+replace x with 1 in *.
+Undo.
+replace x with 0 in *|- *.
+Undo.
+replace x with 0 in *|-.
+Undo.
+replace x with 0 in H0 .
+Undo.
+replace x with 0 in H0 |- * .
+Undo.
+
+replace x with 0 in H,H0 |- * .
+Undo.
+Admitted.
+