ssrpattern: compose nicely with Tactic Notation

5 files changed, 50 insertions, 8 deletions

diff --git a/mathcomp/Make b/mathcomp/Make
index 9f41de1..a235149 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -172,6 +172,7 @@ ssrtest/view_case.v
 ssrtest/wlogletin.v
 ssrtest/wlog_suff.v
 ssrtest/wlong_intro.v
+ssrtest/tacnotationpattern.v
 ssreflect.ml4
 ssreflect.mllib
 ssrmatching.ml4
diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
index 26fd360..a231ee4 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
@@ -1298,12 +1298,25 @@ let ssrpatterntac ist arg gl =
   let (t, uc), concl_x =
     fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in
   let gl, tty = pf_type_of gl t in
-  let concl = mkLetIn (Name (id_of_string "toto"), t, tty, concl_x) in
+  let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in
   Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
 
-TACTIC EXTEND ssrat
-| [ "ssrpattern" ssrpatternarg(arg) ] -> [ Proofview.V82.tactic (ssrpatterntac ist arg) ]
-END
+(* Register "ssrpattern" tactic *)
+let () =
+  let assoc_var s ist =
+  let mltac _ ist =
+    let arg =
+      Genarg.out_gen (topwit wit_ssrpatternarg)
+       (Id.Map.find (Names.Id.of_string "ssrpatternarg") ist.lfun) in
+    Proofview.V82.tactic (ssrpatterntac ist arg) in
+  let name = { mltac_plugin = "ssreflect"; mltac_tactic = "ssrpattern"; } in
+  let () = Tacenv.register_ml_tactic name mltac in
+  let tac =
+    TacFun ([Some (Id.of_string "ssrpatternarg")],
+      TacML (Loc.ghost, name, [])) in
+  let obj () =
+    Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in
+  Mltop.declare_cache_obj obj "ssreflect"
 
 let ssrinstancesof ist arg gl =
   let ok rhs lhs ise = true in
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
index dd135cb..f642811 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
@@ -1285,12 +1285,25 @@ let ssrpatterntac ist arg gl =
   let (t, uc), concl_x =
     fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in
   let gl, tty = pf_type_of gl t in
-  let concl = mkLetIn (Name (id_of_string "toto"), t, tty, concl_x) in
+  let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in
   Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
 
-TACTIC EXTEND ssrat
-| [ "ssrpattern" ssrpatternarg(arg) ] -> [ Proofview.V82.tactic (ssrpatterntac ist arg) ]
-END
+(* Register "ssrpattern" tactic *)
+let () =
+  let assoc_var s ist =
+  let mltac _ ist =
+    let arg =
+      Genarg.out_gen (topwit wit_ssrpatternarg)
+       (Id.Map.find (Names.Id.of_string "ssrpatternarg") ist.lfun) in
+    Proofview.V82.tactic (ssrpatterntac ist arg) in
+  let name = { mltac_plugin = "ssreflect"; mltac_tactic = "ssrpattern"; } in
+  let () = Tacenv.register_ml_tactic name mltac in
+  let tac =
+    TacFun ([Some (Id.of_string "ssrpatternarg")],
+      TacML (Loc.ghost, name, [])) in
+  let obj () =
+    Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in
+  Mltop.declare_cache_obj obj "ssreflect"
 
 let ssrinstancesof ist arg gl =
   let ok rhs lhs ise = true in
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.