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.

---
 theories/Pattern.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'theories/Pattern.v')

diff --git a/theories/Pattern.v b/theories/Pattern.v
index c2ba4162e8..ab3135f189 100644
--- a/theories/Pattern.v
+++ b/theories/Pattern.v
@@ -12,6 +12,11 @@ Ltac2 Type t := pattern.
 
 Ltac2 Type context.
 
+Ltac2 Type 'a constr_match := [
+| ConstrMatchPattern (pattern, constr array -> 'a)
+| ConstrMatchContext (pattern, constr -> constr array -> 'a)
+].
+
 Ltac2 @ external matches : t -> constr -> (ident * constr) list :=
   "ltac2" "pattern_matches".
 (** If the term matches the pattern, returns the bound variables. If it doesn't,
-- 
cgit v1.2.3