diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 2d89b84f5..cc61d4ea8 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -18,6 +18,9 @@ open Extraargs (* Equality *) open Equality +(* V8 TACTIC EXTEND rewrite + [ "rewrite" orient(b) constr_with_bindings(c) ] -> [general_rewrite_bindings b c] +END*) TACTIC EXTEND Rewrite [ "Rewrite" orient(b) constr_with_bindings(c) ] -> [general_rewrite_bindings b c] END @@ -104,6 +107,13 @@ TACTIC EXTEND Inversion -> [ dinv (Some false) c id ] END +(* V8 TACTIC EXTEND inversionclear +| [ "inversion_clear" quantified_hypothesis(id) ] -> [ inv (Some true) id ] +| [ "inversion_clear" quantified_hypothesis(id) "in" ne_ident_list(l) ] + -> [ invIn_gen (Some true) id l] +| [ "dependent" "inversion_clear" quantified_hypothesis(id) with_constr(c) ] + -> [ dinv (Some true) c id ] +END*) TACTIC EXTEND InversionClear | [ "Inversion_clear" quantified_hypothesis(id) ] -> [ inv (Some true) id ] | [ "Inversion_clear" quantified_hypothesis(id) "in" ne_ident_list(l) ] |