diff options
| -rw-r--r-- | tactics/extraargs.ml4 | 6 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 7 |
2 files changed, 9 insertions, 4 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 914e7671f..d9fc8418d 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -57,9 +57,7 @@ ARGUMENT EXTEND raw GLOB_TYPED AS rawconstr_and_expr GLOB_PRINTED BY pr_gen - - [ lconstr(c) ] -> [ c ] - + [ lconstr(c) ] -> [ c ] END type 'id gen_place= ('id * hyp_location_flag,unit) location @@ -100,6 +98,8 @@ ARGUMENT EXTEND hloc GLOB_PRINTED BY pr_loc_place [ ] -> [ ConclLocation () ] + | [ "in" "|-" "*" ] -> + [ ConclLocation () ] | [ "in" ident(id) ] -> [ HypLocation ((Util.dummy_loc,id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 65bed9007..3accfcd0b 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 |