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/Make                 |  1 +
 mathcomp/ssrtest/tacnotationpattern.v | 14 ++++++++++++++
 2 files changed, 15 insertions(+)
 create mode 100644 mathcomp/ssrtest/tacnotationpattern.v

(limited to 'mathcomp/ssrtest')

diff --git a/mathcomp/ssrtest/Make b/mathcomp/ssrtest/Make
index ab4c666..716dc4a 100644
--- a/mathcomp/ssrtest/Make
+++ b/mathcomp/ssrtest/Make
@@ -39,6 +39,7 @@ view_case.v
 wlogletin.v
 wlog_suff.v
 wlong_intro.v
+tacnotationpattern.v
 
 -R ../theories Ssreflect
 -I ../src/
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