From a7c83429db05866dfc9613fc4a488d62d31386fc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Oct 2017 18:42:02 +0200
Subject: Adding a notation for match goal.

---
 tests/matching.v | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'tests')

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