diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 65bed90070..3accfcd0b7 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -244,8 +244,13 @@ END open Tacexpr -TACTIC EXTEND Instantiate +TACTIC EXTEND instantiate [ "Instantiate" "(" integer(i) ":=" raw(c) ")" hloc(hl) ] -> + [instantiate i c hl ] +END + +V7 TACTIC EXTEND instantiate + [ "Instantiate" integer(i) raw(c) hloc(hl) ] -> [ instantiate i c hl ] END |