2 files changed, 54 insertions, 35 deletions
diff --git a/theories/Notations.v b/theories/Notations.v
index 91025ea964..8523c0f524 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -15,22 +15,20 @@ Ltac2 lazy_match0 t pats :=
   let rec interp m := match m with
   | [] => Control.zero Match_failure
   | p :: m =>
-    match p with
-    | Pattern.ConstrMatchPattern pat f =>
-      Control.plus
-        (fun _ =>
-          let bind := Pattern.matches_vect pat t in
-          fun _ => f bind
-        )
-        (fun _ => interp m)
-    | Pattern.ConstrMatchContext pat f =>
-      Control.plus
-        (fun _ =>
-          let ((context, bind)) := Pattern.matches_subterm_vect pat t in
-          fun _ => f context bind
-        )
-        (fun _ => interp m)
-    end
+    let next _ := interp m in
+    let ((knd, pat, f)) := p in
+    let p := match knd with
+    | Pattern.MatchPattern =>
+      (fun _ =>
+        let context := Pattern.empty_context () in
+        let bind := Pattern.matches_vect pat t in
+        fun _ => f context bind)
+    | Pattern.MatchContext =>
+      (fun _ =>
+        let ((context, bind)) := Pattern.matches_subterm_vect pat t in
+        fun _ => f context bind)
+    end in
+    Control.plus p next
   end in
   let ans := Control.once (fun () => interp pats) in
   ans ().
@@ -42,22 +40,20 @@ Ltac2 multi_match0 t pats :=
   let rec interp m := match m with
   | [] => Control.zero Match_failure
   | p :: m =>
-    match p with
-    | Pattern.ConstrMatchPattern pat f =>
-      Control.plus
-        (fun _ =>
-          let bind := Pattern.matches_vect pat t in
-          f bind
-        )
-        (fun _ => interp m)
-    | Pattern.ConstrMatchContext pat f =>
-      Control.plus
-        (fun _ =>
-          let ((context, bind)) := Pattern.matches_subterm_vect pat t in
-          f context bind
-        )
-        (fun _ => interp m)
-    end
+    let next _ := interp m in
+    let ((knd, pat, f)) := p in
+    let p := match knd with
+    | Pattern.MatchPattern =>
+      (fun _ =>
+        let context := Pattern.empty_context () in
+        let bind := Pattern.matches_vect pat t in
+        f context bind)
+    | Pattern.MatchContext =>
+      (fun _ =>
+        let ((context, bind)) := Pattern.matches_subterm_vect pat t in
+        f context bind)
+    end in
+    Control.plus p next
   end in
   interp pats.
 
diff --git a/theories/Pattern.v b/theories/Pattern.v
index a672ad0fe7..fb450d9dfa 100644
--- a/theories/Pattern.v
+++ b/theories/Pattern.v
@@ -12,11 +12,15 @@ Ltac2 Type t := pattern.
 
 Ltac2 Type context.
 
-Ltac2 Type 'a constr_match := [
-| ConstrMatchPattern (pattern, constr array -> 'a)
-| ConstrMatchContext (pattern, context -> constr array -> 'a)
+Ltac2 Type match_kind := [
+| MatchPattern
+| MatchContext
 ].
 
+Ltac2 @ external empty_context : unit -> context :=
+  "ltac2" "pattern_empty_context".
+(** A trivial context only made of the hole. *)
+
 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,
@@ -38,6 +42,25 @@ 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 matches_goal : bool -> (match_kind * t) list -> (match_kind * t) ->
+  ident array * context array * constr array * context :=
+  "ltac2" "pattern_matches_goal".
+(** Given a list of patterns [hpats] for hypotheses and one pattern [cpat] for the
+    conclusion, [matches_goal rev hpats cpat] produces (a stream of) tuples of:
+    - An array of idents, whose size is the length of [hpats], corresponding to the
+      name of matched hypotheses.
+    - An array of contexts, whose size is the length of [hpats], corresponding to
+      the contexts matched for every hypothesis pattern. In case the match kind of
+      a hypothesis was [MatchPattern], the corresponding context is ensured to be empty.
+    - An array of terms, whose size is the total number of pattern variables without
+      duplicates. Terms are ordered by identifier order, e.g. ?a comes before ?b.
+    - A context corresponding to the conclusion, which is ensured to be empty if
+      the kind of [cpat] was [MatchPattern].
+    This produces a backtracking stream of results containing all the possible
+    result combinations. The order of considered hypotheses is reversed if [rev]
+    is true.
+*)
+
 Ltac2 @ external instantiate : context -> constr -> constr :=
   "ltac2" "pattern_instantiate".
 (** Fill the hole of a context with the given term. *)