diff options
| author | Pierre-Marie Pédrot | 2017-09-03 19:45:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-03 23:43:50 +0200 |
| commit | 65daf8fca747d385b2985e4e5e91894738f6fcf1 (patch) | |
| tree | 622f42103d2c79b1742b093ec972016bd4704221 /src/g_ltac2.ml4 | |
| parent | a2302a48a96a6b635f5301f7cc6254acb58211bc (diff) | |
Introducing a macro for constr matching.
Diffstat (limited to 'src/g_ltac2.ml4')
| -rw-r--r-- | src/g_ltac2.ml4 | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index fce4c9e159..5d5bc6b941 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -368,7 +368,7 @@ let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l)) GEXTEND Gram GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag - q_reference q_with_bindings; + q_reference q_with_bindings q_constr_matching; anti: [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ] ; @@ -661,6 +661,25 @@ GEXTEND Gram q_strategy_flag: [ [ flag = strategy_flag -> flag ] ] ; + match_pattern: + [ [ IDENT "context"; id = OPT Prim.ident; + "["; pat = Constr.lconstr_pattern; "]" -> (Some id, pat) + | pat = Constr.lconstr_pattern -> (None, pat) ] ] + ; + match_rule: + [ [ mp = match_pattern; "=>"; tac = tac2expr -> + match mp with + | None, pat -> Loc.tag ~loc:!@loc @@ QConstrMatchPattern (pat, tac) + | Some oid, pat -> Loc.tag ~loc:!@loc @@ QConstrMatchContext (oid, pat, tac) + ] ] + ; + match_list: + [ [ mrl = LIST1 match_rule SEP "|" -> Loc.tag ~loc:!@loc @@ mrl + | "|"; mrl = LIST1 match_rule SEP "|" -> Loc.tag ~loc:!@loc @@ mrl ] ] + ; + q_constr_matching: + [ [ m = match_list -> m ] ] + ; END (** Extension of constr syntax *) |