diff options
Diffstat (limited to 'tactics/extraargs.ml4')
| -rw-r--r-- | tactics/extraargs.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 914e7671f8..d9fc8418d9 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) ")" ] -> |