ssrpattern: compose nicely with Tactic Notation

1 files changed, 14 insertions, 0 deletions

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.