Bug in replace tactics introduced in r9073 (overlap between replace .. with and replace_term).

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

3 files changed, 12 insertions, 19 deletions

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index a3580c3453..498afee99e 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -236,13 +236,3 @@ 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/extraargs.mli b/tactics/extraargs.mli
index 81acf8548b..6534163bbb 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -50,9 +50,3 @@ val glob_in_arg_hyp_to_clause :  (Names.identifier list option * bool)  -> Tacti
 val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e
 val rawwit_by_arg_tac :  raw_tactic_expr option raw_abstract_argument_type
 val wit_by_arg_tac : glob_tactic_expr option closed_abstract_argument_type
-  
-
-
-val replace_term_dir : bool Pcoq.Gram.Entry.e
-val rawwit_replace_term_dir :  bool raw_abstract_argument_type
-val wit_replace_term_dir : bool closed_abstract_argument_type
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 01da2dc110..b10efaec46 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -26,11 +26,20 @@ TACTIC EXTEND replace
 -> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Util.option_map Tacinterp.eval_tactic tac) ]
 END
 
-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)  ]
+TACTIC EXTEND replace_term_left
+  [ "replace"  "->" constr(c) in_arg_hyp(in_hyp) ]
+  -> [ replace_multi_term (Some true) c (glob_in_arg_hyp_to_clause in_hyp)]
 END
 
+TACTIC EXTEND replace_term_right
+  [ "replace"  "<-" constr(c) in_arg_hyp(in_hyp) ]
+  -> [replace_multi_term (Some false) c (glob_in_arg_hyp_to_clause in_hyp)]
+END
+
+TACTIC EXTEND replace_term
+  [ "replace" constr(c) in_arg_hyp(in_hyp) ]
+  -> [ replace_multi_term None c (glob_in_arg_hyp_to_clause in_hyp) ]
+END
 
 TACTIC EXTEND simplify_eq
   [ "simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ]