diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-07-02 12:56:15 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-07-02 12:56:15 +0000 |
| commit | a02d3bbca5244b5d1c4c0d63a39396ae5ce22bac (patch) | |
| tree | f718a81fbe39bb402e24021171324d1d5d76e6ed | |
| parent | 475cc6e4606871a76c4eccf129521ee7740da134 (diff) | |
syntax compatibility fix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5861 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |