Adding a notation for match goal.

1 files changed, 25 insertions, 0 deletions

diff --git a/tests/matching.v b/tests/matching.v
index f43e0121ef..6bc5706da7 100644
--- a/tests/matching.v
+++ b/tests/matching.v
@@ -1,5 +1,12 @@
 Require Import Ltac2.Ltac2 Ltac2.Notations.
 
+Ltac2 Type exn ::= [ Nope ].
+
+Ltac2 check_id id id' := match Ident.equal id id' with
+| true => ()
+| false => Control.throw Nope
+end.
+
 Goal True -> False.
 Proof.
 Fail
@@ -25,3 +32,21 @@ let f c :=
 in
 match! '(nat -> bool) with context [?a] => f a end.
 Abort.
+
+Goal forall (i j : unit) (x y : nat) (b : bool), True.
+Proof.
+Fail match! goal with
+| [ h : ?t, h' : ?t |- _ ] => ()
+end.
+intros i j x y b.
+match! goal with
+| [ h : ?t, h' : ?t |- _ ] =>
+  check_id h @x;
+  check_id h' @y
+end.
+match! reverse goal with
+| [ h : ?t, h' : ?t |- _ ] =>
+  check_id h @j;
+  check_id h' @i
+end.
+Abort.