Wrap ssr tactics into V82.tactic.

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

16 files changed, 139 insertions, 114 deletions

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 6a9a0657a3..692b13c2bb 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -131,7 +131,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:
  let ggenl, tclGENTAC =
    if gviews <> [] && ggenl <> [] then
      let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g ist) (List.hd ggenl) in
-     [], Tacticals.tclTHEN (genstac (ggenl,[]))
+     [], Tacticals.tclTHEN (Proofview.V82.of_tactic (genstac (ggenl,[])))
    else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in
  tclGENTAC (fun gl ->
   match gviews, ggenl with
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index a0d90dcf0d..7e7cd8b4a1 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -569,7 +569,7 @@ let pf_abs_evars gl t = pf_abs_evars2 gl [] t
  * the corresponding lambda looks like (fun evar_i : T(c)) where c is
  * the solution found by ssrautoprop.
  *)
-let ssrautoprop_tac = ref (fun gl -> assert false)
+let ssrautoprop_tac = ref (Proofview.Goal.enter (fun gl -> assert false))
 
 (* Thanks to Arnaud Spiwack for this snippet *)
 let call_on_evar tac e s =
@@ -620,7 +620,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
     if evplist = [] then evlist, [], sigma else
     List.fold_left (fun (ev, evp, sigma) (i, (_,t,_) as p) ->
       try
-        let ng, sigma = call_on_evar !ssrautoprop_tac i sigma in
+        let ng, sigma = call_on_evar (Proofview.V82.of_tactic !ssrautoprop_tac) i sigma in
         if (ng <> []) then errorstrm (str "Should we tell the user?");
         List.filter (fun (j,_) -> j <> i) ev, evp, sigma
       with _ -> ev, p::evp, sigma) (evlist, [], sigma) (List.rev evplist) in
@@ -857,7 +857,8 @@ let pf_abs_ssrterm ?(resolve_typeclasses=false) ist gl t =
 
 let top_id = mk_internal_id "top assumption"
 
-let ssr_n_tac seed n gl =
+let ssr_n_tac seed n =
+  Proofview.Goal.enter begin fun gl ->
   let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in
   let fail msg = CErrors.user_err (Pp.str msg) in
   let tacname =
@@ -867,9 +868,10 @@ let ssr_n_tac seed n gl =
       if n = -1 then fail "The ssreflect library was not loaded"
       else fail ("The tactic "^name^" was not found") in
   let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
-  Proofview.V82.of_tactic (Tacinterp.eval_tactic (Tacexpr.TacArg tacexpr)) gl
+  Tacinterp.eval_tactic (Tacexpr.TacArg tacexpr)
+  end
 
-let donetac n gl = ssr_n_tac "done" n gl
+let donetac n = ssr_n_tac "done" n
 
 open Constrexpr
 open Util
@@ -1181,7 +1183,9 @@ let gentac gen gl =
   else genclrtac cl [c] clr gl
 
 let genstac (gens, clr) =
+  Proofview.V82.tactic ~nf_evars:false begin fun gl ->
   tclTHENLIST (old_cleartac clr :: List.rev_map gentac gens)
+  gl end
 
 let gen_tmp_ids
   ?(ist=Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })) gl
@@ -1217,7 +1221,8 @@ let pfLIFT f =
 (* TASSI: This version of unprotects inlines the unfold tactic definition,
  * since we don't want to wipe out let-ins, and it seems there is no flag
  * to change that behaviour in the standard unfold code *)
-let unprotecttac gl =
+let unprotecttac =
+  Proofview.V82.tactic ~nf_evars:false begin fun gl ->
   let c, gl = pf_mkSsrConst "protect_term" gl in
   let prot, _ = EConstr.destConst (project gl) c in
   Tacticals.onClause (fun idopt ->
@@ -1231,6 +1236,7 @@ let unprotecttac gl =
            CClosure.RedFlags.fFIX;
            CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc))
     allHypsAndConcl gl
+  end
 
 let is_protect hd env sigma =
   let _, protectC = mkSsrConst "protect_term" env sigma in
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 3f92eab0bd..9229b6d384 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -263,7 +263,7 @@ val red_product_skip_id :
   env -> evar_map -> EConstr.t -> EConstr.t
 
 val ssrautoprop_tac :
-           (Evar.t Evd.sigma -> Evar.t list Evd.sigma) ref
+           unit Proofview.tactic ref
 
 val mkProt :
   EConstr.t ->
@@ -306,8 +306,8 @@ val pf_interp_ty :
            (Glob_term.glob_constr * Constrexpr.constr_expr option) ->
            int * EConstr.t * EConstr.t * UState.t
 
-val ssr_n_tac : string -> int -> v82tac
-val donetac : int -> v82tac
+val ssr_n_tac : string -> int -> unit Proofview.tactic
+val donetac : int -> unit Proofview.tactic
 
 val applyn :
            with_evars:bool ->
@@ -361,7 +361,7 @@ val genstac :
   ((Ssrast.ssrhyp list option * Ssrmatching.occ) *
      Ssrmatching.cpattern)
     list * Ssrast.ssrhyp list ->
-  Tacmach.tactic
+  unit Proofview.tactic
 
 val pf_interp_gen :
   bool ->
@@ -392,7 +392,7 @@ val cleartac : ssrhyps -> unit Proofview.tactic
 
 val tclMULT : int * ssrmmod -> Tacmach.tactic -> Tacmach.tactic
 
-val unprotecttac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+val unprotecttac : unit Proofview.tactic
 val is_protect : EConstr.t -> Environ.env -> Evd.evar_map -> bool
 
 val abs_wgen :
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 8f445b4397..8c9dcd9972 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -501,12 +501,13 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with
   let xhavetac id c = Proofview.V82.of_tactic (Tactics.pose_proof (Name id) c) in
   Tacticals.tclTHENLIST [xhavetac id c; injectidl2rtac id (EConstr.mkVar id, NoBindings); Proofview.V82.of_tactic (Tactics.clear [id])]
 
-let is_injection_case c gl =
-  let gl, cty = pfe_type_of gl c in
-  let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in
+let is_injection_case env sigma c =
+  let sigma, cty = Typing.type_of env sigma c in
+  let (mind,_), _ = Tacred.reduce_to_quantified_ind env sigma cty in
   Coqlib.check_ind_ref "core.eq.type" mind
 
-let perform_injection c gl =
+let perform_injection c =
+  Proofview.V82.tactic ~nf_evars:false begin fun gl ->
   let gl, cty = pfe_type_of gl c in
   let mind, t = pf_reduce_to_quantified_ind gl cty in
   let dc, eqt = EConstr.decompose_prod (project gl) t in
@@ -520,7 +521,12 @@ let perform_injection c gl =
   let id_with_ebind = (EConstr.mkVar id, NoBindings) in
   let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in
   Tacticals.tclTHENLAST (Proofview.V82.of_tactic (Tactics.apply (EConstr.compose_lam dc cl1))) injtac gl
+  end
 
-let ssrscase_or_inj_tac c = Proofview.V82.tactic ~nf_evars:false (fun gl ->
-  if is_injection_case c gl then perform_injection c gl
-  else Proofview.V82.of_tactic (casetac c (fun ?seed:_ k -> k)) gl)
+let ssrscase_or_inj_tac c =
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  if is_injection_case env sigma c then perform_injection c
+  else casetac c (fun ?seed:_ k -> k)
+  end
diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli
index 7b9cfed5ba..7f74fc78a2 100644
--- a/plugins/ssr/ssrelim.mli
+++ b/plugins/ssr/ssrelim.mli
@@ -41,10 +41,10 @@ val casetac :
   (?seed:Names.Name.t list array -> unit Proofview.tactic -> unit Proofview.tactic) ->
   unit Proofview.tactic
 
-val is_injection_case : EConstr.t -> Goal.goal Evd.sigma -> bool
+val is_injection_case : Environ.env -> Evd.evar_map -> EConstr.t -> bool
 val perform_injection :
   EConstr.constr ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+  unit Proofview.tactic
 
 val ssrscase_or_inj_tac :
   EConstr.constr ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index d4303e9e8b..1a73bfded0 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -58,12 +58,12 @@ let safe_simpltac n gl =
     let cl= red_safe (tacred_simpl gl) (pf_env gl) (project gl) (pf_concl gl) in
     Proofview.V82.of_tactic (convert_concl_no_check cl) gl
   else
-    ssr_n_tac "simpl" n gl
+    Proofview.V82.of_tactic (ssr_n_tac "simpl" n) gl
 
 let simpltac = function
   | Simpl n -> safe_simpltac n
-  | Cut n -> tclTRY (donetac n)
-  | SimplCut (n,m) -> tclTHEN (safe_simpltac m) (tclTRY (donetac n))
+  | Cut n -> tclTRY (Proofview.V82.of_tactic (donetac n))
+  | SimplCut (n,m) -> tclTHEN (safe_simpltac m) (tclTRY (Proofview.V82.of_tactic (donetac n)))
   | Nop -> tclIDTAC
 
 (** The "congr" tactic *)
@@ -112,7 +112,8 @@ let pf_typecheck t gl =
   let sigma,_  = pf_type_of gl t in
   re_sig [it] sigma
 
-let newssrcongrtac arg ist gl =
+let newssrcongrtac arg ist =
+  Proofview.V82.tactic begin fun gl ->
   ppdebug(lazy Pp.(str"===newcongr==="));
   ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl)));
   (* utils *)
@@ -150,6 +151,7 @@ let newssrcongrtac arg ist gl =
                   ; congrtac (arg, mkRType) ist ])
     (fun _ _ -> errorstrm Pp.(str"Conclusion is not an equality nor an arrow")))
     gl
+  end
 
 (** 7. Rewriting tactics (rewrite, unlock) *)
 
@@ -204,7 +206,7 @@ let simplintac occ rdx sim gl =
         gl in
   match sim with
   | Simpl m -> simptac m gl
-  | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (donetac n)) gl
+  | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (Proofview.V82.of_tactic (donetac n))) gl
   | _ -> simpltac sim gl
 
 let rec get_evalref env sigma c = match EConstr.kind sigma c with
@@ -599,7 +601,8 @@ let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl =
   rwcltac ?under ?map_redex (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
 ;;
 
-let ssrinstancesofrule ist dir arg gl =
+let ssrinstancesofrule ist dir arg =
+  Proofview.V82.tactic begin fun gl ->
   let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
   let rule = interp_term ist gl arg in
   let r_sigma, rules = rwprocess_rule dir rule gl in
@@ -622,6 +625,7 @@ let ssrinstancesofrule ist dir arg gl =
       ignore(find env0 (EConstr.Unsafe.to_constr concl0) 1 ~k:print)
     done; raise NoMatch
   with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); tclIDTAC gl
+  end
 
 let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl
 
@@ -654,7 +658,9 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt)
 (** The "rewrite" tactic *)
 
 let ssrrewritetac ?under ?map_redex ist rwargs =
-  tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs)
+  Proofview.V82.tactic begin fun gl ->
+  tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs) gl
+  end
 
 (** The "unlock" tactic *)
 
@@ -666,7 +672,8 @@ let unfoldtac occ ko t kt gl =
   Proofview.V82.of_tactic
     (convert_concl ~check:true (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl
 
-let unlocktac ist args gl =
+let unlocktac ist args =
+  Proofview.V82.tactic begin fun gl ->
   let utac (occ, gt) gl =
     unfoldtac occ occ (interp_term ist gl gt) (fst gt) gl in
   let locked, gl = pf_mkSsrConst "locked" gl in
@@ -675,3 +682,4 @@ let unlocktac ist args gl =
     (fun gl -> unfoldtac None None (project gl,locked) xInParens gl);
     Proofview.V82.of_tactic (Ssrelim.casetac key (fun ?seed:_ k -> k)) ] in
   tclTHENLIST (List.map utac args @ ktacs) gl
+  end
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index 0bb67c99db..fc2b75b396 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -31,7 +31,7 @@ val simpltac : Ssrast.ssrsimpl -> Tacmach.tactic
 val newssrcongrtac :
   int * Ssrast.ssrterm ->
   Ltac_plugin.Tacinterp.interp_sign ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+  unit Proofview.tactic
 
 
 val mk_rwarg :
@@ -49,7 +49,7 @@ val ssrinstancesofrule :
   Ltac_plugin.Tacinterp.interp_sign ->
   Ssrast.ssrdir ->
   Ssrast.ssrterm ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+  unit Proofview.tactic
 
 (* map_redex (by default the identity on after) is called on the
  * redex (before) and its replacement (after). It is used to
@@ -59,11 +59,11 @@ val ssrrewritetac :
   ?map_redex:(Environ.env -> Evd.evar_map ->
                  before:EConstr.t -> after:EConstr.t -> Evd.evar_map * EConstr.t) ->
   Ltac_plugin.Tacinterp.interp_sign ->
-   ssrrwarg list -> Tacmach.tactic
+   ssrrwarg list -> unit Proofview.tactic
 
 val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic
 
 val unlocktac :
   Ltac_plugin.Tacinterp.interp_sign ->
   (Ssrmatching.occ * Ssrast.ssrterm) list ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+  unit Proofview.tactic
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 43b527c32b..dcf9c1f7db 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -28,15 +28,18 @@ module RelDecl = Context.Rel.Declaration
 
 let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl)
 
-let ssrposetac (id, (_, t)) gl =
+let ssrposetac (id, (_, t)) =
+  Proofview.V82.tactic begin fun gl ->
   let ist, t =
     match t.Ssrast.interp_env with
     | Some ist -> ist, Ssrcommon.ssrterm_of_ast_closure_term t
     | None -> assert false in
   let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in
   posetac id t (pf_merge_uc ucst gl)
+  end
 
-let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
+let ssrsettac id ((_, (pat, pty)), (_, occ)) =
+  Proofview.V82.tactic begin fun gl ->
   let pty = Option.map (fun { Ssrast.body; interp_env } ->
     let ist = Option.get interp_env in
     (mkRHole, Some body), ist) pty in
@@ -57,6 +60,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
   | _ -> c, pfe_type_of gl c in
   let cl' = EConstr.mkLetIn (make_annot (Name id) Sorts.Relevant, c, cty, cl) in
   Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl')) (introid id) gl
+  end
 
 open Util
 
@@ -95,8 +99,9 @@ let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats)
 
 let havetac ist
   (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint)))
-  suff namefst gl
+  suff namefst
 =
+ Proofview.V82.tactic begin fun gl ->
  let concl = pf_concl gl in
  let pats = tclCompileIPats orig_pats in
  let binders = tclCompileIPats binders in
@@ -117,7 +122,7 @@ let havetac ist
  let fixtc =
    not !ssrhaveNOtcresolution &&
    match fk with FwdHint(_,true) -> false | _ -> true in
- let hint = hinttac ist true hint in
+ let hint = Proofview.V82.of_tactic (hinttac ist true hint) in
  let cuttac t gl =
    if transp then
      let have_let, gl = pf_mkSsrConst "ssr_have_let" gl in
@@ -200,7 +205,7 @@ let havetac ist
    | _, true, false -> assert false in
   Tacticals.tclTHENS (cuttac cut) [ Tacticals.tclTHEN sol itac1; itac2 ] gl)
  gl
-;;
+end
 
 let destProd_or_LetIn sigma c =
   match EConstr.kind sigma c with
@@ -208,7 +213,8 @@ let destProd_or_LetIn sigma c =
   | LetIn (n,bo,ty,c) -> RelDecl.LocalDef (n, bo, ty), c
   | _ -> raise DestKO
 
-let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
+let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave =
+  Proofview.V82.tactic begin fun gl ->
   let clr0 = Option.default [] clr0 in
   let pats = tclCompileIPats pats in
   let mkabs gen = abs_wgen false (fun x -> x) gen in
@@ -263,7 +269,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
     Tacticals.tclTHEN
       (Tacticals.tclTHENLIST(List.rev(List.fold_right mkclr gens [old_cleartac clr0])))
       (introstac (List.fold_right mkpats gens [])) in
-  let hinttac = hinttac ist true hint in
+  let hinttac = Proofview.V82.of_tactic (hinttac ist true hint) in
   let cut_kind, fst_goal_tac, snd_goal_tac =
     match suff, ghave with
     | true, `NoGen -> "ssr_wlog", Tacticals.tclTHEN hinttac (tacipat pats), tacigens
@@ -293,15 +299,17 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
       Tacticals.tclTHENLIST [name_general_hyp; tac_specialize; tacipat pats; cleanup]
   in
   Tacticals.tclTHENS (basecuttac cut_kind c) [fst_goal_tac; snd_goal_tac] gl
+  end
 
 (** The "suffice" tactic *)
 
 let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
+  Proofview.V82.tactic begin
   let clr = Option.default [] clr in
   let pats = tclCompileIPats pats in
   let binders = tclCompileIPats binders in
   let simpl = tclCompileIPats simpl in
-  let htac = Tacticals.tclTHEN (introstac pats) (hinttac ist true hint) in
+  let htac = Tacticals.tclTHEN (introstac pats) (Proofview.V82.of_tactic (hinttac ist true hint)) in
   let c = match Ssrcommon.ssrterm_of_ast_closure_term c with
   | (a, (b, Some ct)) ->
     begin match ct.CAst.v with
@@ -318,6 +326,7 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
     let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
     basecuttac "ssr_suff" ty gl in
   Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))]
+  end
 
 open Proofview.Notations
 
@@ -408,7 +417,7 @@ let pretty_rename evar_map term varnames =
   in
     aux term varnames
 
-let overtac = Proofview.V82.tactic (ssr_n_tac "over" ~-1)
+let overtac = ssr_n_tac "over" ~-1
 
 let check_numgoals ?(minus = 0) nh =
   Proofview.numgoals >>= fun ng ->
@@ -492,7 +501,6 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint =
            @ [betaiota])
   in
   let rew =
-    Proofview.V82.tactic
-      (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule])
+    Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]
   in
   rew <*> intro_lock ipats <*> undertacs
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 8aacae39af..2de10837c5 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -16,9 +16,9 @@ open Ltac_plugin
 
 open Ssrast
 
-val ssrsettac :  Id.t -> ((ssrfwdfmt * (Ssrmatching_plugin.Ssrmatching.cpattern * ast_closure_term option)) * ssrdocc) -> v82tac
+val ssrsettac :  Id.t -> ((ssrfwdfmt * (Ssrmatching_plugin.Ssrmatching.cpattern * ast_closure_term option)) * ssrdocc) -> unit Proofview.tactic
 
-val ssrposetac : Id.t * (ssrfwdfmt * ast_closure_term) -> v82tac
+val ssrposetac : Id.t * (ssrfwdfmt * ast_closure_term) -> unit Proofview.tactic
 
 val havetac : ist ->
            bool *
@@ -27,7 +27,7 @@ val havetac : ist ->
             (((Ssrast.ssrfwdkind * 'a) * ast_closure_term) *
              (bool * Tacinterp.Value.t option list))) ->
            bool ->
-           bool -> v82tac
+           bool -> unit Proofview.tactic
 
 val basecuttac :
            string ->
@@ -46,7 +46,7 @@ val wlogtac :
   Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint ->
   bool ->
   [< `Gen of Names.Id.t option option | `NoGen > `NoGen ] ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+  unit Proofview.tactic
 
 val sufftac :
   Ssrast.ist ->
@@ -55,7 +55,7 @@ val sufftac :
     (('a *
         ast_closure_term) *
        (bool * Tacinterp.Value.t option list)) ->
-  Tacmach.tactic
+  unit Proofview.tactic
 
 (* pad_intro (by default false) indicates whether the intro-pattern
    "=> i..." must be turned into "=> [i...|i...|i...|]" (n+1 branches,
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 1edec8e8a0..7fba7ff830 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -337,7 +337,7 @@ let tac_case t =
     Ssrcommon.tacTYPEOF t >>= fun ty ->
     Ssrcommon.tacIS_INJECTION_CASE ~ty t >>= fun is_inj ->
     if is_inj then
-      V82.tactic ~nf_evars:false (Ssrelim.perform_injection t)
+      Ssrelim.perform_injection t
     else
       Goal.enter begin fun g ->
          (Ssrelim.casetac t (fun ?seed k ->
@@ -477,7 +477,7 @@ let rec ipat_tac1 ipat : bool tactic =
 
   | IOpInj ipatss ->
      tclIORPAT (Ssrcommon.tclWITHTOP
-       (fun t -> V82.tactic  ~nf_evars:false (Ssrelim.perform_injection t)))
+       (fun t -> Ssrelim.perform_injection t))
        ipatss
      <*> notTAC
 
@@ -622,7 +622,7 @@ end
 let with_dgens { dgens; gens; clr } maintac = match gens with
   | [] -> with_defective maintac dgens clr
   | gen :: gens ->
-      V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) <*> maintac dgens gen
+      Ssrcommon.genstac (gens, clr) <*> maintac dgens gen
 
 let mkCoqEq env sigma =
   let eq = Coqlib.((build_coq_eq_data ()).eq) in
@@ -647,7 +647,7 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
          | ProdType (_, src, tgt) -> begin
              match kind_of_type sigma src with
              | AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma ->
-                V82.tactic ~nf_evars:false Ssrcommon.unprotecttac <*>
+                Ssrcommon.unprotecttac <*>
                 Ssrcommon.tclINTRO_ID ipat
              | _ -> Ssrcommon.tclINTRO_ANON () <*> intro_eq ()
              end
@@ -700,7 +700,7 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
     | _ -> tclUNIT () in
   let unprotect =
     if eqid <> None && is_rec
-    then V82.tactic ~nf_evars:false Ssrcommon.unprotecttac else tclUNIT () in
+    then Ssrcommon.unprotecttac else tclUNIT () in
   begin match seed with
   | None -> ssrelim
   | Some s -> IpatMachine.tclSEED_SUBGOALS s ssrelim end <*>
@@ -816,7 +816,7 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) =
         Ssrcommon.tacIS_INJECTION_CASE vc >>= fun inj ->
         let simple = (eqid = None && deps = [] && occ = None) in
         if simple && inj then
-          V82.tactic ~nf_evars:false (Ssrelim.perform_injection vc) <*>
+          Ssrelim.perform_injection vc <*>
           Tactics.clear (List.map Ssrcommon.hyp_id clear) <*>
           tclIPATssr ipats
         else
@@ -870,7 +870,7 @@ let tclIPAT ip =
 
 let ssrmovetac = function
   | _::_ as view, (_, ({ gens = lastgen :: gens; clr }, ipats)) ->
-     let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, [])) in
+     let gentac = Ssrcommon.genstac (gens, []) in
      let conclusion _ t clear ccl =
        Tactics.apply_type ~typecheck:true ccl [t] <*>
        Tactics.clear (List.map Ssrcommon.hyp_id clear) in
@@ -884,7 +884,7 @@ let ssrmovetac = function
     let dgentac = with_dgens dgens eqmovetac in
     dgentac <*> tclIPAT (eqmoveipats (IpatMachine.tclCompileIPats [pat]) (IpatMachine.tclCompileIPats ipats))
   | _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) ->
-    let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) in
+    let gentac = Ssrcommon.genstac (gens, clr) in
     gentac <*> tclIPAT (IpatMachine.tclCompileIPats ipats)
   | _, (_, ({ clr }, ipats)) ->
     Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT (IpatMachine.tclCompileIPats ipats)]
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 442b40221b..0307728819 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1611,17 +1611,6 @@ let tactic_expr = Pltac.tactic_expr
 
 (** 1. Utilities *)
 
-(** Tactic-level diagnosis *)
-
-(* debug *)
-
-{
-
-(* Let's play with the new proof engine API *)
-let old_tac = V82.tactic
-
-}
-
 (** Name generation *)
 
 (* Since Coq now does repeated internal checks of its external lexical *)
@@ -1731,18 +1720,20 @@ END
 
 {
 
-let ssrautoprop gl =
+let ssrautoprop =
+  Proofview.Goal.enter begin fun gl ->
   try
     let tacname =
       try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
       with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in
     let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
-    V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
-  with Not_found -> V82.of_tactic (Auto.full_trivial []) gl
+    eval_tactic (Tacexpr.TacArg tacexpr)
+  with Not_found -> Auto.full_trivial []
+  end
 
 let () = ssrautoprop_tac := ssrautoprop
 
-let tclBY tac = Tacticals.tclTHEN tac (donetac ~-1)
+let tclBY tac = Tacticals.New.tclTHEN tac (donetac ~-1)
 
 (** Tactical arguments. *)
 
@@ -1760,7 +1751,7 @@ open Ssrfwd
 }
 
 TACTIC EXTEND ssrtclby
-| [ "by" ssrhintarg(tac) ] -> { V82.tactic (hinttac ist true tac) }
+| [ "by" ssrhintarg(tac) ] -> { hinttac ist true tac }
 END
 
 (* We can't parse "by" in ARGUMENT EXTEND because it will only be made *)
@@ -1778,7 +1769,7 @@ END
 let () = register_ssrtac "tcldo" begin fun args ist -> match args with
 | [arg] ->
   let arg = cast_arg wit_ssrdoarg arg in
-  V82.tactic (ssrdotac ist arg)
+  ssrdotac ist arg
 | _ -> assert false
 end
 
@@ -1827,7 +1818,7 @@ let () = register_ssrtac "tclseq" begin fun args ist -> match args with
   let tac = cast_arg wit_ssrtclarg tac in
   let dir = cast_arg wit_ssrseqdir dir in
   let arg = cast_arg wit_ssrseqarg arg in
-  V82.tactic (tclSEQAT ist tac dir arg)
+  tclSEQAT ist tac dir arg
 | _ -> assert false
 end
 
@@ -2191,9 +2182,9 @@ let vmexacttac pf =
 TACTIC EXTEND ssrexact
 | [ "exact" ssrexactarg(arg) ] -> {
      let views, (gens_clr, _) = arg in
-     V82.tactic (tclBY (V82.of_tactic (inner_ssrapplytac views gens_clr ist))) }
+     tclBY (inner_ssrapplytac views gens_clr ist) }
 | [ "exact" ] -> {
-     V82.tactic (Tacticals.tclORELSE (donetac ~-1) (tclBY (V82.of_tactic apply_top_tac))) }
+     Tacticals.New.tclORELSE (donetac ~-1) (tclBY apply_top_tac) }
 | [ "exact" "<:" lconstr(pf) ] -> { vmexacttac pf }
 END
 
@@ -2220,9 +2211,9 @@ END
 TACTIC EXTEND ssrcongr
 | [ "congr" ssrcongrarg(arg) ] ->
 { let arg, dgens = arg in
-  V82.tactic begin
+  Proofview.Goal.enter begin fun _ ->
     match dgens with
-    | [gens], clr -> Tacticals.tclTHEN (genstac (gens,clr)) (newssrcongrtac arg ist)
+    | [gens], clr -> Tacticals.New.tclTHEN (genstac (gens,clr)) (newssrcongrtac arg ist)
     | _ -> errorstrm (str"Dependent family abstractions not allowed in congr")
   end }
 END
@@ -2342,10 +2333,10 @@ ARGUMENT EXTEND ssrrwarg
 END
 
 TACTIC EXTEND ssrinstofruleL2R
-| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> { V82.tactic (ssrinstancesofrule ist L2R arg) }
+| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> { ssrinstancesofrule ist L2R arg }
 END
 TACTIC EXTEND ssrinstofruleR2L
-| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> { V82.tactic (ssrinstancesofrule ist R2L arg) }
+| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> { ssrinstancesofrule ist R2L arg }
 END
 
 (** Rewrite argument sequence *)
@@ -2395,7 +2386,7 @@ END
 
 TACTIC EXTEND ssrrewrite
   | [ "rewrite" ssrrwargs(args) ssrclauses(clauses) ] ->
-    { tclCLAUSES (old_tac (ssrrewritetac ist args)) clauses }
+    { tclCLAUSES (ssrrewritetac ist args) clauses }
 END
 
 (** The "unlock" tactic *)
@@ -2426,16 +2417,16 @@ END
 
 TACTIC EXTEND ssrunlock
   | [ "unlock" ssrunlockargs(args) ssrclauses(clauses) ] ->
-    { tclCLAUSES (old_tac (unlocktac ist args)) clauses }
+    { tclCLAUSES (unlocktac ist args) clauses }
 END
 
 (** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *)
 
 
 TACTIC EXTEND ssrpose
-| [ "pose" ssrfixfwd(ffwd) ] -> { V82.tactic (ssrposetac ffwd) }
-| [ "pose" ssrcofixfwd(ffwd) ] -> { V82.tactic (ssrposetac ffwd) }
-| [ "pose" ssrfwdid(id) ssrposefwd(fwd) ] -> { V82.tactic (ssrposetac (id, fwd)) }
+| [ "pose" ssrfixfwd(ffwd) ] -> { ssrposetac ffwd }
+| [ "pose" ssrcofixfwd(ffwd) ] -> { ssrposetac ffwd }
+| [ "pose" ssrfwdid(id) ssrposefwd(fwd) ] -> { ssrposetac (id, fwd) }
 END
 
 (** The "set" tactic *)
@@ -2444,7 +2435,7 @@ END
 
 TACTIC EXTEND ssrset
 | [ "set" ssrfwdid(id) ssrsetfwd(fwd) ssrclauses(clauses) ] ->
-  { tclCLAUSES (old_tac (ssrsettac id fwd)) clauses }
+  { tclCLAUSES (ssrsettac id fwd) clauses }
 END
 
 (** The "have" tactic *)
@@ -2471,27 +2462,27 @@ END
 
 TACTIC EXTEND ssrhave
 | [ "have" ssrhavefwdwbinders(fwd) ] ->
-  { V82.tactic (havetac ist fwd false false) }
+  { havetac ist fwd false false }
 END
 
 TACTIC EXTEND ssrhavesuff
 | [ "have" "suff" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] ->
-  { V82.tactic (havetac ist (false,(pats,fwd)) true false) }
+  { havetac ist (false,(pats,fwd)) true false }
 END
 
 TACTIC EXTEND ssrhavesuffices
 | [ "have" "suffices" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] ->
-  { V82.tactic (havetac ist (false,(pats,fwd)) true false) }
+  { havetac ist (false,(pats,fwd)) true false }
 END
 
 TACTIC EXTEND ssrsuffhave
 | [ "suff" "have" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] ->
-  { V82.tactic (havetac ist (false,(pats,fwd)) true true) }
+  { havetac ist (false,(pats,fwd)) true true }
 END
 
 TACTIC EXTEND ssrsufficeshave
 | [ "suffices" "have" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] ->
-  { V82.tactic (havetac ist (false,(pats,fwd)) true true) }
+  { havetac ist (false,(pats,fwd)) true true }
 END
 
 (** The "suffice" tactic *)
@@ -2515,11 +2506,11 @@ END
 
 
 TACTIC EXTEND ssrsuff
-| [ "suff" ssrsufffwd(fwd) ] -> { V82.tactic (sufftac ist fwd) }
+| [ "suff" ssrsufffwd(fwd) ] -> { sufftac ist fwd }
 END
 
 TACTIC EXTEND ssrsuffices
-| [ "suffices" ssrsufffwd(fwd) ] -> { V82.tactic (sufftac ist fwd) }
+| [ "suffices" ssrsufffwd(fwd) ] -> { sufftac ist fwd }
 END
 
 (** The "wlog" (Without Loss Of Generality) tactic *)
@@ -2541,34 +2532,34 @@ END
 
 TACTIC EXTEND ssrwlog
 | [ "wlog" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
-  { V82.tactic (wlogtac ist pats fwd hint false `NoGen) }
+  { wlogtac ist pats fwd hint false `NoGen }
 END
 
 TACTIC EXTEND ssrwlogs
 | [ "wlog" "suff" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
-  { V82.tactic (wlogtac ist pats fwd hint true `NoGen) }
+  { wlogtac ist pats fwd hint true `NoGen }
 END
 
 TACTIC EXTEND ssrwlogss
 | [ "wlog" "suffices" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]->
-  { V82.tactic (wlogtac ist pats fwd hint true `NoGen) }
+  { wlogtac ist pats fwd hint true `NoGen }
 END
 
 TACTIC EXTEND ssrwithoutloss
 | [ "without" "loss" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
-  { V82.tactic (wlogtac ist pats fwd hint false `NoGen) }
+  { wlogtac ist pats fwd hint false `NoGen }
 END
 
 TACTIC EXTEND ssrwithoutlosss
 | [ "without" "loss" "suff"
     ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
-  { V82.tactic (wlogtac ist pats fwd hint true `NoGen) }
+  { wlogtac ist pats fwd hint true `NoGen }
 END
 
 TACTIC EXTEND ssrwithoutlossss
 | [ "without" "loss" "suffices"
     ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]->
-  { V82.tactic (wlogtac ist pats fwd hint true `NoGen) }
+  { wlogtac ist pats fwd hint true `NoGen }
 END
 
 {
@@ -2617,14 +2608,14 @@ TACTIC EXTEND ssrgenhave
 | [ "gen" "have" ssrclear(clr)
     ssr_idcomma(id) ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
   { let pats = augment_preclr clr pats in
-    V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) }
+    wlogtac ist pats fwd hint false (`Gen id) }
 END
 
 TACTIC EXTEND ssrgenhave2
 | [ "generally" "have" ssrclear(clr)
     ssr_idcomma(id) ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
   { let pats = augment_preclr clr pats in
-    V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) }
+    wlogtac ist pats fwd hint false (`Gen id) }
 END
 
 {
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 00d1296291..37e4b625f0 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -45,6 +45,7 @@ let rot_hyps dir i hyps =
   rot (match dir with L2R -> i | R2L -> n - i) [] hyps
 
 let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) =
+  Proofview.V82.tactic begin
   let i = get_index ivar in
   let evtac t = Proofview.V82.of_tactic (ssrevaltac ist t) in
   let tac1 = evtac atac1 in
@@ -57,6 +58,7 @@ let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) =
   | L2R, [], [tac2] when atac3 = None -> Tacticals.tclTHENLAST tac1 tac2
   | L2R, pad, tacs2 -> Tacticals.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3
   | R2L, pad, tacs2 -> Tacticals.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad))
+  end
 
 (** The "in" pseudo-tactical *)(* {{{ **********************************************)
 
@@ -125,7 +127,9 @@ let endclausestac id_map clseq gl_id cl0 gl =
   if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else
   errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical")
 
-let tclCLAUSES tac (gens, clseq) gl =
+let tclCLAUSES tac (gens, clseq) =
+  let tac = Proofview.V82.of_tactic tac in
+  Proofview.V82.tactic begin fun gl ->
   if clseq = InGoal || clseq = InSeqGoal then tac gl else
   let clr_gens = pf_clauseids gl gens clseq in
   let clear = Tacticals.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in
@@ -142,11 +146,13 @@ let tclCLAUSES tac (gens, clseq) gl =
       | _, None -> None) gens in
     endclausestac id_map clseq gl_id cl0 in
   Tacticals.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; clear; tac; endtac]) gl
+  end
 
 (** The "do" tactical. ********************************************************)
 
 let hinttac ist is_by (is_or, atacs) =
-  let dtac = if is_by then donetac ~-1 else Tacticals.tclIDTAC in
+  Proofview.V82.tactic begin
+  let dtac = if is_by then Proofview.V82.of_tactic (donetac ~-1) else Tacticals.tclIDTAC in
   let mktac = function
   | Some atac -> Tacticals.tclTHEN (Proofview.V82.of_tactic (ssrevaltac ist atac)) dtac
   | _ -> dtac in
@@ -154,10 +160,8 @@ let hinttac ist is_by (is_or, atacs) =
   | [] -> if is_or then dtac else Tacticals.tclIDTAC
   | [tac] -> tac
   | tacs -> Tacticals.tclFIRST tacs
+  end
 
 let ssrdotac ist (((n, m), tac), clauses) =
   let mul = get_index n, m in
-  tclCLAUSES (tclMULT mul (hinttac ist false tac)) clauses
-
-let tclCLAUSES tac g_c =
-  Proofview.V82.(tactic (tclCLAUSES (of_tactic tac) g_c))
+  tclCLAUSES (Proofview.V82.tactic (tclMULT mul (Proofview.V82.of_tactic (hinttac ist false tac)))) clauses
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index c5b0deb752..f907ac3801 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -20,7 +20,7 @@ val tclSEQAT :
   int Locus.or_var *
     (('a * Tacinterp.Value.t option list) *
        Tacinterp.Value.t option) ->
-  Tacmach.tactic
+  unit Proofview.tactic
 
 val tclCLAUSES :
   unit Proofview.tactic ->
@@ -33,7 +33,7 @@ val tclCLAUSES :
 
 val hinttac :
            Tacinterp.interp_sign ->
-           bool -> bool * Tacinterp.Value.t option list -> Ssrast.v82tac
+           bool -> bool * Tacinterp.Value.t option list -> unit Proofview.tactic
 
 val ssrdotac :
   Tacinterp.interp_sign ->
@@ -44,5 +44,5 @@ val ssrdotac :
            Ssrmatching.cpattern option)
           option)
        list * Ssrast.ssrclseq) ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+  unit Proofview.tactic
 
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. *)