Update v8.5 plugin to fix math-comp/math-comp#61

4 files changed, 8 insertions, 9 deletions

diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib b/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib
index 006b70f..dee851c 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib
@@ -1,2 +1 @@
-Ssrmatching
 Ssreflect
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
index 658966b..ebc4de9 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
@@ -49,11 +49,11 @@ open Notation_ops
 open Locus
 open Locusops
 
-DECLARE PLUGIN "ssreflect"
+DECLARE PLUGIN "ssrmatching_plugin"
 
 type loc = Loc.t
 let dummy_loc = Loc.ghost
-let errorstrm = Errors.errorlabstrm "ssreflect"
+let errorstrm = Errors.errorlabstrm "ssrmatching"
 let loc_error loc msg = Errors.user_err_loc (loc, msg, str msg)
 
 (* 0 cost pp function. Active only if env variable SSRDEBUG is set *)
@@ -1334,14 +1334,14 @@ let () =
       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 name = { mltac_plugin = "ssrmatching_plugin"; 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"
+  Mltop.declare_cache_obj obj "ssrmatching_plugin"
 
 let ssrinstancesof ist arg gl =
   let ok rhs lhs ise = true in
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v
index 369ffaf..c20c846 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v
@@ -1,9 +1,6 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
+Declare ML Module "ssrmatching_plugin".
 
 Module SsrMatchingSyntax.
 
@@ -25,3 +22,5 @@ Notation LHS := (X in X = _)%pattern.
 End SsrMatchingSyntax.
 
 Export SsrMatchingSyntax.
+
+Tactic Notation "ssrpattern" ssrpatternarg(p) := ssrpattern p .
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching_plugin.mllib b/mathcomp/ssreflect/plugin/v8.5/ssrmatching_plugin.mllib
new file mode 100644
index 0000000..5fb1f15
--- /dev/null
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching_plugin.mllib
@@ -0,0 +1 @@
+Ssrmatching