diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 4068289eb9..06493804f7 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -123,12 +123,20 @@ TACTIC EXTEND AutorewriteV7 [ autorewrite Refiner.tclIDTAC l ] | [ "AutoRewrite" "[" ne_preident_list(l) "]" "using" tactic(t) ] -> [ autorewrite (snd t) l ] +| [ "AutoRewrite" "[" ne_preident_list(l) "]" "in" ident(id) ] -> + [ autorewrite_in id Refiner.tclIDTAC l ] +| [ "AutoRewrite" "[" ne_preident_list(l) "]" "in" ident(id) "using" tactic(t) ] -> + [ autorewrite_in id (snd t) l ] END TACTIC EXTEND AutorewriteV8 [ "AutoRewrite" "with" ne_preident_list(l) ] -> [ autorewrite Refiner.tclIDTAC l ] | [ "AutoRewrite" "with" ne_preident_list(l) "using" tactic(t) ] -> [ autorewrite (snd t) l ] +| [ "AutoRewrite" "with" ne_preident_list(l) "in" ident(id) ] -> + [ autorewrite_in id Refiner.tclIDTAC l ] +| [ "AutoRewrite" "with" ne_preident_list(l) "in" ident(id) "using" tactic(t) ] -> + [ autorewrite_in id (snd t) l ] END let add_rewrite_hint name ort t lcsr = |