From 102cfe76bc42d3139c79eca59eb782fcf644317b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 Sep 2017 23:52:12 +0200
Subject: Implementing lazy matching over terms.

---
 theories/Pattern.v | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'theories/Pattern.v')

diff --git a/theories/Pattern.v b/theories/Pattern.v
index ab3135f189..a672ad0fe7 100644
--- a/theories/Pattern.v
+++ b/theories/Pattern.v
@@ -14,7 +14,7 @@ Ltac2 Type context.
 
 Ltac2 Type 'a constr_match := [
 | ConstrMatchPattern (pattern, constr array -> 'a)
-| ConstrMatchContext (pattern, constr -> constr array -> 'a)
+| ConstrMatchContext (pattern, context -> constr array -> 'a)
 ].
 
 Ltac2 @ external matches : t -> constr -> (ident * constr) list :=
@@ -30,6 +30,14 @@ Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) li
     value compared to [matches] is the context of the match, to be filled with
     the instantiate function. *)
 
+Ltac2 @ external matches_vect : t -> constr -> constr array :=
+  "ltac2" "pattern_matches_vect".
+(** Internal version of [matches] that does not return the identifiers. *)
+
+Ltac2 @ external matches_subterm_vect : t -> constr -> context * constr array :=
+  "ltac2" "pattern_matches_subterm_vect".
+(** Internal version of [matches_subterms] that does not return the identifiers. *)
+
 Ltac2 @ external instantiate : context -> constr -> constr :=
   "ltac2" "pattern_instantiate".
 (** Fill the hole of a context with the given term. *)
-- 
cgit v1.2.3