diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 4 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 12 |
3 files changed, 12 insertions, 6 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index e2e6795f7..8df91da24 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -218,7 +218,7 @@ GEXTEND Gram CGeneralization (!@loc, Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> CGeneralization (!@loc, Explicit, None, c) - | "$("; tac = Tactic.tactic; ")$" -> + | "ltac:"; "("; tac = Tactic.tactic_expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in CHole (!@loc, None, IntroAnonymous, Some arg) ] ] diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index a4dba506d..4a9ca23f1 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -134,8 +134,8 @@ GEXTEND Gram ; (* Tactic arguments *) tactic_arg: - [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a - | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n) + [ [ "ltac:"; a = tactic_expr LEVEL "0" -> arg_of_expr a + | "ltac:"; n = natural -> TacGeneric (genarg_of_int n) | a = tactic_top_or_arg -> a | r = reference -> Reference r | c = Constr.constr -> ConstrMayEval (ConstrTerm c) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index c94ac846f..b7559a198 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -296,11 +296,17 @@ GEXTEND Gram | "**" -> !@loc, IntroForthcoming false ]] ; simple_intropattern: + [ [ pat = simple_intropattern_closed; l = LIST0 ["/"; c = constr -> c] -> + let loc0,pat = pat in + let f c pat = + let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in + IntroAction (IntroApplyOn (c,(loc,pat))) in + !@loc, List.fold_right f l pat ] ] + ; + simple_intropattern_closed: [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat) | pat = equality_intropattern -> !@loc, IntroAction pat | "_" -> !@loc, IntroAction IntroWildcard - | pat = simple_intropattern; "/"; c = constr -> - !@loc, IntroAction (IntroApplyOn (c,pat)) | pat = naming_intropattern -> !@loc, IntroNaming pat ] ] ; simple_binding: @@ -399,7 +405,7 @@ GEXTEND Gram | -> [] ] ] ; in_hyp_as: - [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (None,id,ipat) + [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat) | -> None ] ] ; orient: |