From fb9ccea7f34b7fcd01a5f0f97b5c52b188154f5b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 25 Feb 2016 15:20:35 +0100
Subject: ssrpattern: compose nicely with Tactic Notation

---
 mathcomp/ssrtest/tacnotationpattern.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 mathcomp/ssrtest/tacnotationpattern.v

(limited to 'mathcomp/ssrtest/tacnotationpattern.v')

diff --git a/mathcomp/ssrtest/tacnotationpattern.v b/mathcomp/ssrtest/tacnotationpattern.v
new file mode 100644
index 0000000..13de4bc
--- /dev/null
+++ b/mathcomp/ssrtest/tacnotationpattern.v
@@ -0,0 +1,14 @@
+Require Import mathcomp.ssreflect.ssreflect.
+Tactic Notation "at" ssrpatternarg(p) tactic(t)
+ := 
+    ssrpattern p; let top := fresh in intro top;
+    t top; try unfold top in * |- *; try clear top.
+
+Goal forall x y, x + y = 4.
+intros.
+at [RHS] (fun top => remember top as E eqn:E_def).
+match goal with
+| |- x + y = E => idtac
+| |- _ => fail
+end.
+Admitted.
-- 
cgit v1.2.3