From 65daf8fca747d385b2985e4e5e91894738f6fcf1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 Sep 2017 19:45:23 +0200
Subject: Introducing a macro for constr matching.

---
 src/g_ltac2.ml4 | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

(limited to 'src/g_ltac2.ml4')

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 *)
-- 
cgit v1.2.3