diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 8e5e1f1fb8..b7559a1989 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: |