diff options
| -rw-r--r-- | tactics/extraargs.ml4 | 10 | ||||
| -rw-r--r-- | tactics/extraargs.mli | 6 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 15 |
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 ] |