diff options
| author | Hugo Herbelin | 2015-12-02 12:10:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-02 18:34:11 +0100 |
| commit | 6ab4479dfa0f9b8fd4df4342fdfdab6c25b62fb7 (patch) | |
| tree | 65ccc8e483adcd60bf1efd3bc3992d045ad90def /parsing | |
| parent | cc153dbbe45d5cf7f6ebfef6010adcc4f5bb568c (diff) | |
Improving syntax of pat/constr introduction pattern so that
pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.
Open to other suggestions of syntax though.
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: |