Wrap ssr tactics into V82.tactic.

Porting them is still to be done, but at least we don't rely on the wrapper
everywhere.

3 files changed, 5 insertions, 3 deletions

diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 33e523a4a4..2252435658 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -107,7 +107,7 @@ ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY { pr_rpattern }
 END
 
 TACTIC EXTEND ssrinstoftpat
-| [ "ssrinstancesoftpat" cpattern(arg) ] -> { Proofview.V82.tactic (ssrinstancesof arg) }
+| [ "ssrinstancesoftpat" cpattern(arg) ] -> { ssrinstancesof arg }
 END
 
 {
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index d5a781e472..6a36959e83 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -1315,7 +1315,8 @@ let () =
     Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in
   Mltop.declare_cache_obj obj "ssrmatching_plugin"
 
-let ssrinstancesof arg gl =
+let ssrinstancesof arg =
+  Proofview.V82.tactic begin fun gl ->
   let ok rhs lhs ise = true in
 (*   not (equal lhs (Evarutil.nf_evar ise rhs)) in *)
   let env, sigma, concl = pf_env gl, project gl, pf_concl gl in
@@ -1334,6 +1335,7 @@ let ssrinstancesof arg gl =
       ignore(find env concl 1 ~k:print)
     done; raise NoMatch
   with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl
+  end
 
 module Internal =
 struct
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 31b414cc42..176dfa92b2 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -230,7 +230,7 @@ val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma
 (* One can also "Set SsrMatchingDebug" from a .v *)
 val debug : bool -> unit
 
-val ssrinstancesof : cpattern -> Tacmach.tactic
+val ssrinstancesof : cpattern -> unit Proofview.tactic
 
 (** Functions used for grammar extensions. Do not use. *)