Merge PR #12227: Spring cleaning of the tactic compatibility layer

Reviewed-by: gares

29 files changed, 729 insertions, 540 deletions

diff --git a/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh b/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh
new file mode 100644
index 0000000000..0f8daf418c
--- /dev/null
+++ b/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12227" ] || [ "$CI_BRANCH" = "refiner-rm-v82" ]; then
+
+    equations_CI_REF="refiner-rm-v82"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 020ab9307d..52c6c5d0f9 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -164,14 +164,17 @@ module Btauto = struct
 
   let reify env t = lapp eval [|convert_env env; convert t|]
 
-  let print_counterexample p penv gl =
+  let print_counterexample p penv =
+  Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
     let var = lapp witness [|p|] in
     let var = EConstr.of_constr var in
     (* Compute an assignment that dissatisfies the goal *)
-    let redfun, _ = Redexpr.reduction_of_red_expr (Refiner.pf_env gl) Genredexpr.(CbvVm None) in
-    let _, var = redfun Refiner.(pf_env gl) Refiner.(project gl) var in
+    let redfun, _ = Redexpr.reduction_of_red_expr env Genredexpr.(CbvVm None) in
+    let _, var = redfun env sigma var in
     let var = EConstr.Unsafe.to_constr var in
-    let rec to_list l = match decomp_term (Tacmach.project gl) l with
+    let rec to_list l = match decomp_term sigma l with
     | App (c, _)
       when c === (Lazy.force CoqList._nil) -> []
     | App (c, [|_; h; t|])
@@ -196,7 +199,6 @@ module Btauto = struct
         let assign = List.combine penv var in
         let map_msg (key, v) =
           let b = if v then str "true" else str "false" in
-          let sigma, env = Tacmach.project gl, Tacmach.pf_env gl in
           let term = Printer.pr_constr_env env sigma key in
           term ++ spc () ++ str ":=" ++ spc () ++ b
         in
@@ -205,7 +207,8 @@ module Btauto = struct
         str "Not a tautology:" ++ spc () ++ l
       with e when CErrors.noncritical e -> (str "Not a tautology")
     in
-    Tacticals.tclFAIL 0 msg gl
+    Tacticals.New.tclFAIL 0 msg
+  end
 
   let try_unification env =
     Proofview.Goal.enter begin fun gl ->
@@ -216,7 +219,7 @@ module Btauto = struct
       match t with
       | App (c, [|typ; p; _|]) when c === eq ->
       (* should be an equality [@eq poly ?p (Cst false)] *)
-          let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in
+          let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (print_counterexample p env) in
           tac
       | _ ->
           let msg = str "Btauto: Internal error" in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 7b2ce671a3..f4200854c2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -41,7 +41,10 @@ let observe_tac s = observe_tac (fun _ _ -> Pp.str s)
 let finish_proof dynamic_infos g =
   observe_tac "finish" (Proofview.V82.of_tactic assumption) g
 
-let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)
+let refine c =
+  Proofview.V82.of_tactic
+    (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c))
+
 let thin l = Proofview.V82.of_tactic (Tactics.clear l)
 let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v
 
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 6a9a0657a3..42b9248979 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -55,18 +55,18 @@ let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl)
 let interp_nbargs ist gl rc =
   try
     let rc6 = mkRApp rc (mkRHoles 6) in
-    let sigma, t = interp_open_constr ist gl (rc6, None) in
+    let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc6, None) in
     let si = sig_it gl in
     let gl = re_sig si sigma in
-    6 + Ssrcommon.nbargs_open_constr gl t
+    6 + Ssrcommon.nbargs_open_constr (pf_env gl) t
   with _ -> 5
 
 let interp_view_nbimps ist gl rc =
   try
-    let sigma, t = interp_open_constr ist gl (rc, None) in
+    let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc, None) in
     let si = sig_it gl in
     let gl = re_sig si sigma in
-    let pl, c = splay_open_constr gl t in
+    let pl, c = splay_open_constr (pf_env gl) t in
     if Ssrcommon.isAppInd (pf_env gl) (project gl) c then List.length pl else (-(List.length pl))
   with _ -> 0
 
@@ -88,7 +88,7 @@ let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c)
 let apply_rconstr ?ist t gl =
 (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *)
   let n = match ist, DAst.get t with
-    | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id)
+    | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs (pf_env gl) (project gl) (EConstr.mkVar id)
     | Some ist, _ -> interp_nbargs ist gl t
     | _ -> anomaly "apply_rconstr without ist and not RVar" in
   let mkRlemma i = mkRApp t (mkRHoles i) in
@@ -97,7 +97,7 @@ let apply_rconstr ?ist t gl =
     if i > n then
       errorstrm Pp.(str"Cannot apply lemma "++pf_pr_glob_constr gl t)
     else try pf_match gl (mkRlemma i) (OfType cl) with _ -> loop (i + 1) in
-  refine_with (loop 0) gl
+  Proofview.V82.of_tactic (refine_with (loop 0)) gl
 
 let mkRAppView ist gl rv gv =
   let nb_view_imps = interp_view_nbimps ist gl rv in
@@ -112,18 +112,20 @@ let refine_interp_apply_view dbl ist gl gv =
     interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in
   let rec loop = function
   | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv)
-  | h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in
+  | h :: hs -> (try Proofview.V82.of_tactic (refine_with (snd (interp_with h))) gl with _ -> loop hs) in
   loop (pair dbl (Ssrview.AdaptorDb.get dbl) @
         if dbl = Ssrview.AdaptorDb.Equivalence
         then pair Ssrview.AdaptorDb.Backward (Ssrview.AdaptorDb.(get Backward))
         else [])
 
 let apply_top_tac =
-  Tacticals.tclTHENLIST [
+  Proofview.Goal.enter begin fun _ ->
+  Tacticals.New.tclTHENLIST [
     introid top_id;
-    apply_rconstr (mkRVar top_id);
-    old_cleartac [SsrHyp(None,top_id)]
+    Proofview.V82.tactic (apply_rconstr (mkRVar top_id));
+    cleartac [SsrHyp(None,top_id)]
   ]
+  end
 
 let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:false (fun gl ->
  let _, clr = interp_hyps ist gl gclr in
@@ -131,7 +133,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
@@ -148,9 +150,9 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:
   | [], [agens] ->
     let clr', (sigma, lemma) = interp_agens ist gl agens in
     let gl = pf_merge_uc_of sigma gl in
-    Tacticals.tclTHENLIST [old_cleartac clr; refine_with ~beta:true lemma; old_cleartac clr'] gl
+    Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr']) gl
   | _, _ ->
-     Tacticals.tclTHENLIST [apply_top_tac; old_cleartac clr] gl) gl
+    Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [apply_top_tac; cleartac clr]) gl) gl
 )
 
-let apply_top_tac = Proofview.V82.tactic ~nf_evars:false apply_top_tac
+let apply_top_tac = apply_top_tac
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 134a9e4b36..e05c4c26dd 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -221,8 +221,8 @@ let intern_term ist env (_, c) = glob_constr ist env c
 (* FUNCLASS, which is probably just as well since these can     *)
 (* lead to infinite arities.                                    *)
 
-let splay_open_constr gl (sigma, c) =
-  let env = pf_env gl in let t = Retyping.get_type_of env sigma c in
+let splay_open_constr env (sigma, c) =
+  let t = Retyping.get_type_of env sigma c in
   Reductionops.splay_prod env sigma t
 
 let isAppInd env sigma c =
@@ -253,11 +253,11 @@ let interp_refine ist gl rc =
   (sigma, (sigma, c))
 
 
-let interp_open_constr ist gl gc =
-  let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in
-  (project gl, (sigma, c))
+let interp_open_constr env sigma0 ist gc =
+  let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist env sigma0 (gc, Tactypes.NoBindings) in
+  (sigma0, (sigma, c))
 
-let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c)
+let interp_term env sigma ist (_, c) = snd (interp_open_constr env sigma ist c)
 
 let of_ftactic ftac gl =
   let r = ref None in
@@ -322,10 +322,10 @@ let ssrdgens_of_parsed_dgens = function
   | _ -> assert false
 
 
-let nbargs_open_constr gl oc =
-  let pl, _ = splay_open_constr gl oc in List.length pl
+let nbargs_open_constr env oc =
+  let pl, _ = splay_open_constr env oc in List.length pl
 
-let pf_nbargs gl c = nbargs_open_constr gl (project gl, c)
+let pf_nbargs env sigma c = nbargs_open_constr env (sigma, c)
 
 let internal_names = ref []
 let add_internal_name pt = internal_names := pt :: !internal_names
@@ -521,10 +521,10 @@ let resolve_typeclasses ~where ~fail env sigma =
 let nf_evar sigma t =
   EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t))
 
-let pf_abs_evars2 gl rigid (sigma, c0) =
+let abs_evars2 env sigma0 rigid (sigma, c0) =
   let c0 = EConstr.to_constr ~abort_on_undefined_evars:false sigma c0 in
-  let sigma0, ucst = project gl, Evd.evar_universe_context sigma in
-  let nenv = env_size (pf_env gl) in
+  let sigma0, ucst = sigma0, Evd.evar_universe_context sigma in
+  let nenv = env_size env in
   let abs_evar n k =
     let evi = Evd.find sigma k in
     let concl = EConstr.Unsafe.to_constr evi.evar_concl in
@@ -558,6 +558,11 @@ let pf_abs_evars2 gl rigid (sigma, c0) =
   | [] -> c in
   List.length evlist, EConstr.of_constr (loop (get 1 c0) 1 evlist), List.map fst evlist, ucst
 
+let pf_abs_evars2 gl rigid c =
+  abs_evars2 (pf_env gl) (project gl) rigid c
+
+let abs_evars env sigma t = abs_evars2 env sigma [] t
+
 let pf_abs_evars gl t = pf_abs_evars2 gl [] t
 
 
@@ -569,7 +574,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 =
@@ -581,12 +586,11 @@ open Pp
 let pp _ = () (* FIXME *)
 module Intset = Evar.Set
 
-let pf_abs_evars_pirrel gl (sigma, c0) =
+let abs_evars_pirrel env sigma0 (sigma, c0) =
   pp(lazy(str"==PF_ABS_EVARS_PIRREL=="));
-  pp(lazy(str"c0= " ++ Printer.pr_constr_env (pf_env gl) sigma c0));
-  let sigma0 = project gl in
+  pp(lazy(str"c0= " ++ Printer.pr_constr_env env sigma c0));
   let c0 = nf_evar sigma0 (nf_evar sigma c0) in
-  let nenv = env_size (pf_env gl) in
+  let nenv = env_size env in
   let abs_evar n k =
     let evi = Evd.find sigma k in
     let concl = EConstr.Unsafe.to_constr evi.evar_concl in
@@ -602,13 +606,13 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
     let n = max 0 (List.length a - nenv) in
     let k_ty =
       Retyping.get_sort_family_of
-        (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in
+        env sigma (Evd.evar_concl (Evd.find sigma k)) in
     let is_prop = k_ty = InProp in
     let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t
   | _ -> Constr.fold put evlist c in
   let evlist = put [] c0 in
   if evlist = [] then 0, c0 else
-  let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (pf_env gl) (project gl) (EConstr.of_constr t)) in
+  let pr_constr t = Printer.pr_econstr_env env sigma (Reductionops.nf_beta env sigma0 (EConstr.of_constr t)) in
   pp(lazy(str"evlist=" ++ pr_list (fun () -> str";")
     (fun (k,_) -> Evar.print k) evlist));
   let evplist =
@@ -620,7 +624,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
@@ -667,6 +671,9 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   pp(lazy(str"res= " ++ pr_constr res));
   List.length evlist, res
 
+let pf_abs_evars_pirrel gl c =
+  abs_evars_pirrel (pf_env gl) (project gl) c
+
 (* Strip all non-essential dependencies from an abstracted term, generating *)
 (* standard names for the abstracted holes.                                 *)
 
@@ -678,7 +685,8 @@ let nb_evar_deps = function
     (try int_of_string (String.sub s m (String.length s - 1 - m)) with _ -> 0)
   | _ -> 0
 
-let pf_type_id gl t = Id.of_string (Namegen.hdchar (pf_env gl) (project gl) t)
+let type_id env sigma t = Id.of_string (Namegen.hdchar env sigma t)
+let pf_type_id gl t = type_id (pf_env gl) (project gl) t
 let pfe_type_of gl t =
   let sigma, ty = pf_type_of gl t in
   re_sig (sig_it gl) sigma, ty
@@ -693,7 +701,7 @@ let pf_type_of gl t =
   let sigma, ty = pf_type_of gl (EConstr.of_constr t) in
   re_sig (sig_it gl)  sigma, EConstr.Unsafe.to_constr ty
 
-let pf_abs_cterm gl n c0 =
+let abs_cterm env sigma n c0 =
   if n <= 0 then c0 else
   let c0 = EConstr.Unsafe.to_constr c0 in
   let noargs = [|0|] in
@@ -725,13 +733,15 @@ let pf_abs_cterm gl n c0 =
       let na' = List.length dl in
       eva.(i) <- Array.of_list (na - na' :: dl);
       let x' =
-        if na' = 0 then Name (pf_type_id gl (EConstr.of_constr t2)) else mk_evar_name na' in
+        if na' = 0 then Name (type_id env sigma (EConstr.of_constr t2)) else mk_evar_name na' in
       mkLambda ({x with binder_name=x'}, t2, strip_evars (i + 1) c1)
 (*      if noccurn 1 c2 then lift (-1) c2 else
       mkLambda (Name (pf_type_id gl t2), t2, c2) *)
     | _ -> strip i c in
   EConstr.of_constr (strip_evars 0 c0)
 
+let pf_abs_cterm gl n c0 = abs_cterm (pf_env gl) (project gl) n c0
+
 (* }}} *)
 
 let pf_merge_uc uc gl =
@@ -835,7 +845,7 @@ open Locus
 let rewritetac ?(under=false) dir c =
   (* Due to the new optional arg ?tac, application shouldn't be too partial *)
   let open Proofview.Notations in
-  Proofview.V82.of_tactic begin
+  Proofview.Goal.enter begin fun _ ->
       Equality.general_rewrite (dir = L2R) AllOccurrences true false c <*>
         if under then Proofview.cycle 1 else Proofview.tclUNIT ()
   end
@@ -845,7 +855,7 @@ let rewritetac ?(under=false) dir c =
 type name_hint = (int * EConstr.types array) option ref
 
 let pf_abs_ssrterm ?(resolve_typeclasses=false) ist gl t =
-  let sigma, ct as t = interp_term ist gl t in
+  let sigma, ct as t = interp_term (pf_env gl) (project gl) ist t in
   let sigma, _ as t =
     let env = pf_env gl in
     if not resolve_typeclasses then t
@@ -857,7 +867,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 +878,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
@@ -890,7 +902,7 @@ let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty)
 let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = []
 let rec isCxHoles = function ({ CAst.v = CHole _ }, None) :: ch -> isCxHoles ch | _ -> false
 
-let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
+let pf_interp_ty ?(resolve_typeclasses=false) env sigma0 ist ty =
    let n_binders = ref 0 in
    let ty = match ty with
    | a, (t, None) ->
@@ -915,15 +927,14 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
      | LetInType(n,v,ty,t) -> decr n_binders; mkLetIn (n, v, ty, aux t)
      | _ -> anomaly "pf_interp_ty: ssr Type cast deleted by typecheck" in
      sigma, aux t in
-   let sigma, cty as ty = strip_cast (interp_term ist gl ty) in
+   let sigma, cty as ty = strip_cast (interp_term env sigma0 ist ty) in
    let ty =
-     let env = pf_env gl in
      if not resolve_typeclasses then ty
      else
        let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
        sigma, Evarutil.nf_evar sigma cty in
-   let n, c, _, ucst = pf_abs_evars gl ty in
-   let lam_c = pf_abs_cterm gl n c in
+   let n, c, _, ucst = abs_evars env sigma0 ty in
+   let lam_c = abs_cterm env sigma0 n c in
    let ctx, c = EConstr.decompose_lam_n_assum sigma n lam_c in
    n, EConstr.it_mkProd_or_LetIn c ctx, lam_c, ucst
 ;;
@@ -981,7 +992,8 @@ let dependent_apply_error =
  *
  * Refiner.refiner that does not handle metas with a non ground type but works
  * with dependently typed higher order metas. *)
-let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t gl =
+let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t =
+  Proofview.V82.tactic begin fun gl ->
   if with_evars then
     let refine gl =
       let t, ty, args, gl = pf_saturate ?beta ~bi_types:true gl t n in
@@ -1014,16 +1026,22 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t g
     pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
     Proofview.(V82.of_tactic
       (Tacticals.New.tclTHENLIST [
-         V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t));
+         Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t);
          (if first_goes_last then cycle 1 else tclUNIT ())
       ])) gl
+  end
 
-let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
+let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc =
+  let open Proofview.Notations in
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
   let uct = Evd.evar_universe_context (fst oc) in
-  let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in
-  let gl = pf_unsafe_merge_uc uct gl in
-  try applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
-  with e when CErrors.noncritical e -> raise dependent_apply_error
+  let n, oc = abs_evars_pirrel env sigma (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in
+  Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*>
+  Proofview.tclOR (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc))
+    (fun _ -> Proofview.tclZERO dependent_apply_error)
+  end
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
 (* The user is supposed to Require Import ssreflect or Require ssreflect   *)
@@ -1041,23 +1059,24 @@ let rec fst_prod red tac = Proofview.Goal.enter begin fun gl ->
          else Tacticals.New.tclTHEN Tactics.hnf_in_concl (fst_prod true tac)
 end
 
-let introid ?(orig=ref Anonymous) name = tclTHEN (fun gl ->
-   let g, env = Tacmach.pf_concl gl, pf_env gl in
-   let sigma = project gl in
+let introid ?(orig=ref Anonymous) name =
+  let open Proofview.Notations in
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let g = Proofview.Goal.concl gl in
    match EConstr.kind sigma g with
    | App (hd, _) when EConstr.isLambda sigma hd ->
-      Proofview.V82.of_tactic (convert_concl_no_check (Reductionops.whd_beta sigma g)) gl
-   | _ -> tclIDTAC gl)
-  (Proofview.V82.of_tactic
-    (fst_prod false (fun id -> orig := id; Tactics.intro_mustbe_force name)))
-;;
+      convert_concl_no_check (Reductionops.whd_beta sigma g)
+   | _ -> Tacticals.New.tclIDTAC
+  end <*>
+    (fst_prod false (fun id -> orig := id; Tactics.intro_mustbe_force name))
 
 let anontac decl gl =
   let id =  match RelDecl.get_name decl with
   | Name id ->
     if is_discharged_id id then id else mk_anon_id (Id.to_string id) (Tacmach.pf_ids_of_hyps gl)
   | _ -> mk_anon_id ssr_anon_hyp (Tacmach.pf_ids_of_hyps gl) in
-  introid id gl
+  Proofview.V82.of_tactic (introid id) gl
 
 let rec intro_anon gl =
   try anontac (List.hd (fst (EConstr.decompose_prod_n_assum (project gl) 1 (Tacmach.pf_concl gl)))) gl
@@ -1085,16 +1104,17 @@ let interp_clr sigma = function
 let tclID tac = tac
 
 let tclDOTRY n tac =
+  let open Tacticals.New in
   if n <= 0 then tclIDTAC else
-  let rec loop i gl =
-    if i = n then tclTRY tac gl else
-    tclTRY (tclTHEN tac (loop (i + 1))) gl in
+  let rec loop i =
+    if i = n then tclTRY tac else
+    tclTRY (tclTHEN tac (loop (i + 1))) in
   loop 1
 
 let tclDO n tac =
   let prefix i = str"At iteration " ++ int i ++ str": " in
   let tac_err_at i gl =
-    try tac gl
+    try Proofview.V82.of_tactic tac gl
     with
     | CErrors.UserError (l, s) as e ->
       let _, info = Exninfo.capture e in
@@ -1105,11 +1125,15 @@ let tclDO n tac =
   let rec loop i gl =
     if i = n then tac_err_at i gl else
     (tclTHEN (tac_err_at i) (loop (i + 1))) gl in
-  loop 1
+  Proofview.V82.tactic ~nf_evars:false (loop 1)
+
+let tclAT_LEAST_ONCE t =
+  let open Tacticals.New in
+  tclTHEN t (tclREPEAT t)
 
 let tclMULT = function
-  | 0, May  -> tclREPEAT
-  | 1, May  -> tclTRY
+  | 0, May  -> Tacticals.New.tclREPEAT
+  | 1, May  -> Tacticals.New.tclTRY
   | n, May  -> tclDOTRY n
   | 0, Must -> tclAT_LEAST_ONCE
   | n, Must when n > 1 -> tclDO n
@@ -1124,7 +1148,7 @@ let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr)
 
 (* XXX the k of the redex should percolate out *)
 let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
-  let pat = interp_cpattern gl t None in (* UGLY API *)
+  let pat = interp_cpattern (pf_env gl) (project gl) t None in (* UGLY API *)
   let gl = pf_merge_uc_of (fst pat) gl in
   let cl, env, sigma = Tacmach.pf_concl gl, pf_env gl, project gl in
   let (c, ucst), cl =
@@ -1171,7 +1195,8 @@ let genclrtac cl cs clr =
            gl))
     (old_cleartac clr)
 
-let gentac gen gl =
+let gentac gen =
+  Proofview.V82.tactic begin fun gl ->
 (*   ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *)
   let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux gl false gen in
   ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c));
@@ -1179,9 +1204,10 @@ let gentac gen gl =
   if conv
   then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl
   else genclrtac cl [c] clr gl
+  end
 
 let genstac (gens, clr) =
-  tclTHENLIST (old_cleartac clr :: List.rev_map gentac gens)
+  Tacticals.New.tclTHENLIST (cleartac clr :: List.rev_map gentac gens)
 
 let gen_tmp_ids
   ?(ist=Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })) gl
@@ -1191,7 +1217,7 @@ let gen_tmp_ids
     (tclTHENLIST
       (List.map (fun (id,orig_ref) ->
         tclTHEN
-        (gentac ((None,Some(false,[])),cpattern_of_id id))
+        (Proofview.V82.of_tactic (gentac ((None,Some(false,[])),cpattern_of_id id)))
         (rename_hd_prod orig_ref))
       ctx.tmp_ids) gl)
 ;;
@@ -1214,24 +1240,6 @@ let pfLIFT f =
     Proofview.tclUNIT x
 ;;
 
-(* 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 c, gl = pf_mkSsrConst "protect_term" gl in
-  let prot, _ = EConstr.destConst (project gl) c in
-  Tacticals.onClause (fun idopt ->
-    let hyploc = Option.map (fun id -> id, InHyp) idopt in
-    Proofview.V82.of_tactic (Tactics.reduct_option ~check:false
-      (Reductionops.clos_norm_flags
-        (CClosure.RedFlags.mkflags
-          [CClosure.RedFlags.fBETA;
-           CClosure.RedFlags.fCONST prot;
-           CClosure.RedFlags.fMATCH;
-           CClosure.RedFlags.fFIX;
-           CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc))
-    allHypsAndConcl gl
-
 let is_protect hd env sigma =
   let _, protectC = mkSsrConst "protect_term" env sigma in
   EConstr.eq_constr_nounivs sigma hd protectC
@@ -1259,7 +1267,7 @@ let abs_wgen keep_let f gen (gl,args,c) =
      gl, EConstr.mkVar x :: args, prod
   | _, Some ((x, "@"), Some p) ->
      let x = hoi_id x in
-     let cp = interp_cpattern gl p None in
+     let cp = interp_cpattern (pf_env gl) (project gl) p None in
      let gl = pf_merge_uc_of (fst cp) gl in
      let (t, ucst), c =
        try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1
@@ -1272,7 +1280,7 @@ let abs_wgen keep_let f gen (gl,args,c) =
      pf_merge_uc ucst gl, args, EConstr.mkLetIn(make_annot (Name (f x)) r, ut, ty, c)
   | _, Some ((x, _), Some p) ->
      let x = hoi_id x in
-     let cp = interp_cpattern gl p None in
+     let cp = interp_cpattern (pf_env gl) (project gl) p None in
      let gl = pf_merge_uc_of (fst cp) gl in
      let (t, ucst), c =
        try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1
@@ -1287,8 +1295,8 @@ let abs_wgen keep_let f gen (gl,args,c) =
 let clr_of_wgen gen clrs = match gen with
   | clr, Some ((x, _), None) ->
      let x = hoi_id x in
-     old_cleartac clr :: old_cleartac [SsrHyp(Loc.tag x)] :: clrs
-  | clr, _ -> old_cleartac clr :: clrs
+     cleartac clr :: cleartac [SsrHyp(Loc.tag x)] :: clrs
+  | clr, _ -> cleartac clr :: clrs
 
 
 let reduct_in_concl ~check t = Tactics.reduct_in_concl ~check (t, DEFAULTcast)
@@ -1321,7 +1329,8 @@ end
 
 let tacREDUCE_TO_QUANTIFIED_IND ty =
   tacSIGMA >>= fun gl ->
-  tclUNIT (Tacmach.pf_reduce_to_quantified_ind gl ty)
+  try tclUNIT (Tacmach.pf_reduce_to_quantified_ind gl ty)
+  with e -> tclZERO e
 
 let tacTYPEOF c = Goal.enter_one ~__LOC__ (fun g ->
   let sigma, env = Goal.sigma g, Goal.env g in
@@ -1460,7 +1469,7 @@ end
 
 let tacINTERP_CPATTERN cp =
   tacSIGMA >>= begin fun gl ->
-  tclUNIT (Ssrmatching.interp_cpattern gl cp None)
+  tclUNIT (Ssrmatching.interp_cpattern (pf_env gl) (project gl) cp None)
 end
 
 let tacUNIFY a b =
@@ -1488,12 +1497,38 @@ let tclWITHTOP tac = Goal.enter begin fun gl ->
   Tactics.clear [top]
 end
 
-let tacMK_SSR_CONST name = Goal.enter_one ~__LOC__ begin fun g ->
-  let sigma, env = Goal.(sigma g, env g) in
-  let sigma, c = mkSsrConst name env sigma in
-  Unsafe.tclEVARS sigma <*>
-  tclUNIT c
-end
+let tacMK_SSR_CONST name =
+  Proofview.tclENV >>= fun env ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match mkSsrConst name env sigma with
+  | sigma, c -> Unsafe.tclEVARS sigma <*> tclUNIT c
+  | exception e when CErrors.noncritical e ->
+    tclLIFT (Proofview.NonLogical.raise (e, Exninfo.null))
+
+let tacDEST_CONST c =
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match EConstr.destConst sigma c with
+  | c, _ -> tclUNIT c
+  | exception e when CErrors.noncritical e ->
+    tclLIFT (Proofview.NonLogical.raise (e, Exninfo.null))
+
+(* 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 =
+  tacMK_SSR_CONST "protect_term" >>= tacDEST_CONST >>= fun prot ->
+  Tacticals.New.onClause (fun idopt ->
+    let hyploc = Option.map (fun id -> id, InHyp) idopt in
+    Tactics.reduct_option ~check:false
+      (Reductionops.clos_norm_flags
+        (CClosure.RedFlags.mkflags
+          [CClosure.RedFlags.fBETA;
+           CClosure.RedFlags.fCONST prot;
+           CClosure.RedFlags.fMATCH;
+           CClosure.RedFlags.fFIX;
+           CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc)
+    allHypsAndConcl
+
 
 module type StateType = sig
   type state
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 3f92eab0bd..d1ad24496e 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -131,7 +131,8 @@ val pf_intern_term :
     ssrterm -> Glob_term.glob_constr
 
 val interp_term :
-  Tacinterp.interp_sign -> Goal.goal Evd.sigma ->
+  Environ.env -> Evd.evar_map ->
+  Tacinterp.interp_sign ->
     ssrterm -> evar_map * EConstr.t
 
 val interp_wit :
@@ -145,7 +146,8 @@ val interp_refine :
     Glob_term.glob_constr -> evar_map * (evar_map * EConstr.constr)
 
 val interp_open_constr :
-  Tacinterp.interp_sign -> Goal.goal Evd.sigma ->
+  Environ.env -> Evd.evar_map ->
+  Tacinterp.interp_sign ->
     Genintern.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t)
 
 val pf_e_type_of :
@@ -153,7 +155,7 @@ val pf_e_type_of :
   EConstr.constr -> Goal.goal Evd.sigma * EConstr.types
 
 val splay_open_constr :
-           Goal.goal Evd.sigma ->
+           Environ.env ->
            evar_map * EConstr.t ->
            (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t
 val isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool
@@ -179,8 +181,23 @@ val mk_internal_id : string -> Id.t
 val mk_tagged_id : string -> int -> Id.t
 val mk_evar_name : int -> Name.t
 val ssr_anon_hyp : string
+val type_id : Environ.env -> Evd.evar_map -> EConstr.types -> Id.t
 val pf_type_id :  Goal.goal Evd.sigma -> EConstr.types -> Id.t
 
+val abs_evars :
+           Environ.env -> Evd.evar_map ->
+           evar_map * EConstr.t ->
+           int * EConstr.t * Evar.t list *
+           UState.t
+val abs_evars2 : (* ssr2 *)
+           Environ.env -> Evd.evar_map -> Evar.t list ->
+           evar_map * EConstr.t ->
+           int * EConstr.t * Evar.t list *
+           UState.t
+val abs_cterm :
+           Environ.env -> Evd.evar_map -> int -> EConstr.t -> EConstr.t
+
+
 val pf_abs_evars :
            Goal.goal Evd.sigma ->
            evar_map * EConstr.t ->
@@ -216,15 +233,8 @@ val pf_abs_prod :
            EConstr.t -> Goal.goal Evd.sigma * EConstr.types
 
 val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
-val mkSsrConst :
-           string ->
-           env -> evar_map -> evar_map * EConstr.t
-val pf_mkSsrConst :
-           string ->
-           Goal.goal Evd.sigma ->
-           EConstr.t * Goal.goal Evd.sigma
-val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx
 
+val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx
 
 val pf_fresh_global :
            GlobRef.t ->
@@ -239,11 +249,14 @@ val ssrqid : string -> Libnames.qualid
 val new_tmp_id :
   tac_ctx -> (Names.Id.t * Name.t ref) * tac_ctx
 val mk_anon_id : string -> Id.t list -> Id.t
+val abs_evars_pirrel :
+           Environ.env -> Evd.evar_map ->
+           evar_map * Constr.constr -> int * Constr.constr
 val pf_abs_evars_pirrel :
            Goal.goal Evd.sigma ->
            evar_map * Constr.constr -> int * Constr.constr
-val nbargs_open_constr : Goal.goal Evd.sigma -> Evd.evar_map * EConstr.t -> int
-val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int
+val nbargs_open_constr : Environ.env -> Evd.evar_map * EConstr.t -> int
+val pf_nbargs : Environ.env -> Evd.evar_map -> EConstr.t -> int
 val gen_tmp_ids :
            ?ist:Geninterp.interp_sign ->
            (Goal.goal * tac_ctx) Evd.sigma ->
@@ -263,7 +276,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 ->
@@ -300,14 +313,15 @@ val pf_abs_ssrterm :
 
 val pf_interp_ty :
            ?resolve_typeclasses:bool ->
+           Environ.env ->
+           Evd.evar_map ->
            Tacinterp.interp_sign ->
-           Goal.goal Evd.sigma ->
            Ssrast.ssrtermkind *
            (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 ->
@@ -315,7 +329,7 @@ val applyn :
            ?with_shelve:bool ->
            ?first_goes_last:bool ->
            int ->
-           EConstr.t -> v82tac
+           EConstr.t -> unit Proofview.tactic
 exception NotEnoughProducts
 val pf_saturate :
            ?beta:bool ->
@@ -339,7 +353,7 @@ val refine_with :
            ?first_goes_last:bool ->
            ?beta:bool ->
            ?with_evars:bool ->
-           evar_map * EConstr.t -> v82tac
+           evar_map * EConstr.t -> unit Proofview.tactic
 
 val pf_resolve_typeclasses :
   where:EConstr.t ->
@@ -350,18 +364,18 @@ val resolve_typeclasses :
 
 (*********************** Wrapped Coq  tactics *****************************)
 
-val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> tactic
+val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> unit Proofview.tactic
 
 type name_hint = (int * EConstr.types array) option ref
 
 val gentac :
-   Ssrast.ssrdocc * Ssrmatching.cpattern -> v82tac
+   Ssrast.ssrdocc * Ssrmatching.cpattern -> unit Proofview.tactic
 
 val genstac :
   ((Ssrast.ssrhyp list option * Ssrmatching.occ) *
      Ssrmatching.cpattern)
     list * Ssrast.ssrhyp list ->
-  Tacmach.tactic
+  unit Proofview.tactic
 
 val pf_interp_gen :
   bool ->
@@ -378,7 +392,7 @@ val pfLIFT
 
 (** Basic tactics *)
 
-val introid : ?orig:Name.t ref -> Id.t -> v82tac
+val introid : ?orig:Name.t ref -> Id.t -> unit Proofview.tactic
 val intro_anon : v82tac
 
 val interp_clr :
@@ -390,9 +404,9 @@ val genclrtac :
 val old_cleartac : ssrhyps -> v82tac
 val cleartac : ssrhyps -> unit Proofview.tactic
 
-val tclMULT : int * ssrmmod -> Tacmach.tactic -> Tacmach.tactic
+val tclMULT : int * ssrmmod -> unit Proofview.tactic -> unit Proofview.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 :
@@ -407,7 +421,7 @@ val abs_wgen :
 
 val clr_of_wgen :
   ssrhyps * ((ssrhyp_or_id * 'a) * 'b option) option ->
-  Proofview.V82.tac list -> Proofview.V82.tac list
+  unit Proofview.tactic list -> unit Proofview.tactic list
 
 
 val unfold : EConstr.t list -> unit Proofview.tactic
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index b44600a8cf..8e75ba7a2b 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -183,7 +183,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
         else
           let c = Option.get oc in let gl, c_ty = pfe_type_of gl c in
           let pc = match c_gen with
-            | Some p -> interp_cpattern orig_gl p None
+            | Some p -> interp_cpattern (pf_env orig_gl) (project orig_gl) p None
             | _ -> mkTpat gl c in
           Some(c, c_ty, pc), gl in
       seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
@@ -233,7 +233,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
         pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in
       let pred = List.assoc pred_id elim_args in
       let pc = match n_c_args, c_gen with
-        | 0, Some p -> interp_cpattern orig_gl p None
+        | 0, Some p -> interp_cpattern (pf_env orig_gl) (project orig_gl) p None
         | _ -> mkTpat gl c in
       let cty = Some (c, c_ty, pc) in
       let elimty = Reductionops.whd_all env (project gl) elimty in
@@ -312,7 +312,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
     let rec loop patterns clr i = function
       | [],[] -> patterns, clr, gl
       | ((oclr, occ), t):: deps, inf_t :: inf_deps ->
-          let p = interp_cpattern orig_gl t None in
+          let p = interp_cpattern (pf_env orig_gl) (project orig_gl) t None in
           let clr_t =
             interp_clr (project gl) (oclr,(tag_of_cpattern t,EConstr.of_constr (fst (redex_of_pattern env p)))) in
           (* if we are the index for the equation we do not clear *)
@@ -392,10 +392,15 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
           let erefl = fire_subst gl erefl in
           let erefl_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl in
           let eq_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl_ty in
-          let gen_eq_tac s =
+          let gen_eq_tac =
+            let open Proofview.Notations in
+            Proofview.Goal.enter begin fun s ->
+            let sigma = Proofview.Goal.sigma s in
             let open Evd in
-            let sigma = merge_universe_context s.sigma (evar_universe_context (project gl)) in
-            apply_type new_concl [erefl] { s with sigma }
+            let sigma = merge_universe_context sigma (evar_universe_context (project gl)) in
+            Proofview.Unsafe.tclEVARS sigma <*>
+            Tactics.apply_type ~typecheck:true new_concl [erefl]
+            end
           in
           gen_eq_tac, eq_ty, gl in
         let rel = k + if c_is_head_p then 1 else 0 in
@@ -403,7 +408,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
         let concl = EConstr.mkArrow src Sorts.Relevant (EConstr.Vars.lift 1 concl) in
         let clr = if deps <> [] then clr else [] in
         concl, gen_eq_tac, clr, gl
-    | _ -> concl, Tacticals.tclIDTAC, clr, gl in
+    | _ -> concl, Tacticals.New.tclIDTAC, clr, gl in
     let mk_lam t r = EConstr.mkLambda_or_LetIn r t in
     let concl = List.fold_left mk_lam concl pred_rctx in
     let gl, concl =
@@ -453,9 +458,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
 
   let elim_tac =
     Tacticals.New.tclTHENLIST [
-      Proofview.V82.tactic (refine_with ~with_evars:false elim);
+      refine_with ~with_evars:false elim;
       cleartac clr] in
-  let gen_eq_tac = Proofview.V82.tactic gen_eq_tac in
   Tacticals.New.tclTHENLIST [gen_eq_tac; elim_intro_tac ?seed:(Some seed) what eqid elim_tac is_rec clr]
 ;;
 
@@ -467,19 +471,22 @@ let casetac x k =
   let k ?seed _what _eqid elim_tac _is_rec _clr = k ?seed elim_tac in
   ssrelim ~is_case:true [] (`EConstr ([],None,x)) None k
 
-let pf_nb_prod gl = nb_prod (project gl) (pf_concl gl)
-
 let rev_id = mk_internal_id "rev concl"
 let injecteq_id = mk_internal_id "injection equation"
 
-let revtoptac n0 gl =
-  let n = pf_nb_prod gl - n0 in
-  let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in
+let revtoptac n0 =
+  Proofview.Goal.enter begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
+  let concl = Proofview.Goal.concl gl in
+  let n = nb_prod sigma concl - n0 in
+  let dc, cl = EConstr.decompose_prod_n_assum sigma n concl in
   let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in
   let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in
-  Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl
+  Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])))
+  end
 
-let equality_inj l b id c gl =
+let equality_inj l b id c =
+  Proofview.V82.tactic begin fun gl ->
   let msg = ref "" in
   try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
   with
@@ -490,37 +497,53 @@ let equality_inj l b id c gl =
        !msg = "Nothing to inject." ->
     Feedback.msg_warning (Pp.str !msg);
     discharge_hyp (id, (id, "")) gl
+  end
 
-let injectidl2rtac id c gl =
-  Tacticals.tclTHEN (equality_inj None true id c) (revtoptac (pf_nb_prod gl)) gl
+let injectidl2rtac id c =
+  Proofview.Goal.enter begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
+  let concl = Proofview.Goal.concl gl in
+  Tacticals.New.tclTHEN (equality_inj None true id c) (revtoptac (nb_prod sigma concl))
+  end
 
 let injectl2rtac sigma c = match EConstr.kind sigma c with
 | Var id -> injectidl2rtac id (EConstr.mkVar id, NoBindings)
 | _ ->
   let id = injecteq_id in
-  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 xhavetac id c = Tactics.pose_proof (Name id) c in
+  Tacticals.New.tclTHENLIST [xhavetac id c; injectidl2rtac id (EConstr.mkVar id, NoBindings); 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 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
-  if dc = [] then injectl2rtac (project gl) c gl else
-  if not (EConstr.Vars.closed0 (project gl) eqt) then
+let perform_injection c =
+  let open Proofview.Notations in
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let sigma, cty = Typing.type_of env sigma c in
+  let mind, t = Tacred.reduce_to_quantified_ind env sigma cty in
+  let dc, eqt = EConstr.decompose_prod sigma t in
+  if dc = [] then injectl2rtac sigma c else
+  if not (EConstr.Vars.closed0 sigma eqt) then
     CErrors.user_err (Pp.str "can't decompose a quantified equality") else
-  let cl = pf_concl gl in let n = List.length dc in
+  let cl = Proofview.Goal.concl gl in
+  let n = List.length dc in
   let c_eq = mkEtaApp c n 2 in
   let cl1 = EConstr.mkLambda EConstr.(make_annot Anonymous Sorts.Relevant, mkArrow eqt Sorts.Relevant cl, mkApp (mkRel 1, [|c_eq|])) in
   let id = injecteq_id in
   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
+  let injtac = Tacticals.New.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in
+  Proofview.Unsafe.tclEVARS sigma <*>
+  Tacticals.New.tclTHENLAST (Tactics.apply (EConstr.compose_lam dc cl1)) injtac
+  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..ab07dd5be9 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -42,29 +42,36 @@ let () =
 
 (* We must avoid zeta-converting any "let"s created by the "in" tactical. *)
 
-let tacred_simpl gl =
+let tacred_simpl env =
   let simpl_expr =
     Genredexpr.(
       Simpl(Redops.make_red_flag[FBeta;FMatch;FZeta;FDeltaBut []],None)) in
-  let esimpl, _ = Redexpr.reduction_of_red_expr (pf_env gl) simpl_expr in
+  let esimpl, _ = Redexpr.reduction_of_red_expr env simpl_expr in
   let esimpl e sigma c =
     let (_,t) = esimpl e sigma c in
     t in
   let simpl env sigma c = (esimpl env sigma c) in
   simpl
 
-let safe_simpltac n gl =
+let safe_simpltac n =
   if n = ~-1 then
-    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
+    Proofview.Goal.enter begin fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      let concl = Proofview.Goal.concl gl in
+      let cl = red_safe (tacred_simpl env) env sigma concl in
+      convert_concl_no_check cl
+    end
   else
-    ssr_n_tac "simpl" n gl
+    ssr_n_tac "simpl" n
 
 let simpltac = function
   | Simpl n -> safe_simpltac n
-  | Cut n -> tclTRY (donetac n)
-  | SimplCut (n,m) -> tclTHEN (safe_simpltac m) (tclTRY (donetac n))
-  | Nop -> tclIDTAC
+  | Cut n -> Tacticals.New.tclTRY (donetac n)
+  | SimplCut (n,m) -> Tacticals.New.tclTHEN (safe_simpltac m) (Tacticals.New.tclTRY (donetac n))
+  | Nop -> Tacticals.New.tclIDTAC
+
+let simpltac s = Proofview.Goal.enter (fun _ -> simpltac s)
 
 (** The "congr" tactic *)
 
@@ -87,13 +94,13 @@ let pattern_id = mk_internal_id "pattern value"
 let congrtac ((n, t), ty) ist gl =
   ppdebug(lazy (Pp.str"===congr==="));
   ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl)));
-  let sigma, _ as it = interp_term ist gl t in
+  let sigma, _ as it = interp_term (pf_env gl) (project gl) ist t in
   let gl = pf_merge_uc_of sigma gl in
   let _, f, _, _ucst = pf_abs_evars gl it in
   let ist' = {ist with lfun =
     Id.Map.add pattern_id (Tacinterp.Value.of_constr f) Id.Map.empty } in
   let rf = mkRltacVar pattern_id in
-  let m = pf_nbargs gl f in
+  let m = pf_nbargs (pf_env gl) (project gl) f in
   let _, cf = if n > 0 then
     match interp_congrarg_at ist' gl n rf ty m with
     | Some cf -> cf
@@ -105,14 +112,18 @@ let congrtac ((n, t), ty) ist gl =
       | Some cf -> cf
       | None -> loop (i + 1) in
       loop 1 in
-  tclTHEN (refine_with cf) (tclTRY (Proofview.V82.of_tactic Tactics.reflexivity)) gl
+  Proofview.V82.of_tactic Tacticals.New.(tclTHEN (refine_with cf) (tclTRY Tactics.reflexivity)) gl
 
 let pf_typecheck t gl =
   let it = sig_it gl in
   let sigma,_  = pf_type_of gl t in
   re_sig [it] sigma
 
-let newssrcongrtac arg ist gl =
+let newssrcongrtac arg ist =
+  let open Proofview.Notations in
+  Proofview.Goal.enter_one ~__LOC__ begin fun _g ->
+    (Ssrcommon.tacMK_SSR_CONST "ssr_congr_arrow") end >>= fun arr ->
+  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 *)
@@ -129,7 +140,6 @@ let newssrcongrtac arg ist gl =
     let sigma = Evd.create_evar_defs sigma in
     let (sigma, x) = Evarutil.new_evar env sigma ty in
     x, re_sig si sigma in
-  let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in
   let ssr_congr lr = EConstr.mkApp (arr, lr) in
   let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
   (* here the two cases: simple equality or arrow *)
@@ -150,6 +160,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) *)
 
@@ -188,24 +199,28 @@ let mk_rwarg (d, (n, _ as m)) ((clr, occ as docc), rx) (rt, _ as r) : ssrrwarg =
 let norwmult = L2R, nomult
 let norwocc = noclr, None
 
-let simplintac occ rdx sim gl =
-  let simptac m gl =
+let simplintac occ rdx sim =
+  let simptac m =
+    Proofview.Goal.enter begin fun gl ->
     if m <> ~-1 then begin
       if rdx <> None then
         CErrors.user_err (Pp.str "Custom simpl tactic does not support patterns");
       if occ <> None then
         CErrors.user_err (Pp.str "Custom simpl tactic does not support occurrence numbers");
-      simpltac (Simpl m) gl
+      simpltac (Simpl m)
     end else
-      let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
+      let sigma0, concl0, env0 = Proofview.Goal.(sigma gl, concl gl, env gl) in
       let simp env c _ _ = EConstr.Unsafe.to_constr (red_safe Tacred.simpl env sigma0 (EConstr.of_constr c)) in
-      Proofview.V82.of_tactic
-        (convert_concl_no_check (EConstr.of_constr (eval_pattern env0 sigma0 (EConstr.Unsafe.to_constr concl0) rdx occ simp)))
-        gl in
+      convert_concl_no_check (EConstr.of_constr (eval_pattern env0 sigma0 (EConstr.to_constr ~abort_on_undefined_evars:false sigma0 concl0) rdx occ simp))
+    end
+  in
+  let open Tacticals.New in
+  Proofview.Goal.enter begin fun _ ->
   match sim with
-  | Simpl m -> simptac m gl
-  | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (donetac n)) gl
-  | _ -> simpltac sim gl
+  | Simpl m -> simptac m
+  | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (donetac n))
+  | _ -> simpltac sim
+  end
 
 let rec get_evalref env sigma c = match EConstr.kind sigma c with
   | Var id -> EvalVarRef id
@@ -233,7 +248,8 @@ let all_ok _ _ = true
 let fake_pmatcher_end () =
   mkProp, L2R, (Evd.empty, UState.empty, mkProp)
 
-let unfoldintac occ rdx t (kt,_) gl =
+let unfoldintac occ rdx t (kt,_) =
+  Proofview.V82.tactic begin fun gl ->
   let fs sigma x = Reductionops.nf_evar sigma x in
   let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
   let (sigma, t), const = strip_unfold_term env0 t kt in
@@ -286,9 +302,10 @@ let unfoldintac occ rdx t (kt,_) gl =
     with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_econstr_pat env0 sigma t) in
   let _ = conclude () in
   Proofview.V82.of_tactic (convert_concl ~check:true concl) gl
-;;
+  end
 
-let foldtac occ rdx ft gl =
+let foldtac occ rdx ft =
+  Proofview.V82.tactic begin fun gl ->
   let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
   let sigma, t = ft in
   let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
@@ -313,7 +330,7 @@ let foldtac occ rdx ft gl =
   let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in
   let _ = conclude () in
   Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.of_constr concl)) gl
-;;
+  end
 
 let converse_dir = function L2R -> R2L | R2L -> L2R
 
@@ -337,7 +354,8 @@ exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_e
 
 let id_map_redex _ sigma ~before:_ ~after = sigma, after
 
-let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
+let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty =
+  Proofview.V82.tactic begin fun gl ->
 (*   ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *)
   let env = pf_env gl in
   let beta = Reductionops.clos_norm_flags CClosure.beta env sigma in
@@ -369,8 +387,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
   in
   ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof));
   ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
-  try refine_with
-    ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof) gl
+  try Proofview.V82.of_tactic (refine_with
+    ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl
   with _ ->
     (* we generate a msg like: "Unable to find an instance for the variable" *)
     let hd_ty, miss = match EConstr.kind sigma c with
@@ -393,62 +411,73 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
     | _ -> anomaly "rewrite rule not an application" in
     errorstrm Pp.(Himsg.explain_refiner_error env sigma (Logic.UnresolvedBindings miss)++
       (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty))
-;;
+  end
+
+let pf_merge_uc_of s sigma =
+  Evd.merge_universe_context sigma (Evd.evar_universe_context s)
 
-let rwcltac ?under ?map_redex cl rdx dir sr gl =
+let rwcltac ?under ?map_redex cl rdx dir sr =
+  let open Proofview.Notations in
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma0 = Proofview.Goal.sigma gl in
   let sr =
     let sigma, r = sr in
-    let sigma = resolve_typeclasses ~where:r ~fail:false (pf_env gl) sigma in
+    let sigma = resolve_typeclasses ~where:r ~fail:false env sigma in
     sigma, r in
-  let n, r_n,_, ucst = pf_abs_evars gl sr in
-  let r_n' = pf_abs_cterm gl n r_n in
+  let n, r_n,_, ucst = abs_evars env sigma0 sr in
+  let r_n' = abs_cterm env sigma0 n r_n in
   let r' = EConstr.Vars.subst_var pattern_id r_n' in
-  let gl = pf_unsafe_merge_uc ucst gl in
-  let rdxt = Retyping.get_type_of (pf_env gl) (fst sr) rdx in
+  let sigma0 = Evd.set_universe_context sigma0 ucst in
+  let rdxt = Retyping.get_type_of env (fst sr) rdx in
 (*         ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *)
-        ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr)));
-  let cvtac, rwtac, gl =
-    if EConstr.Vars.closed0 (project gl) r' then
-      let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in
+        ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr)));
+  let cvtac, rwtac, sigma0 =
+    if EConstr.Vars.closed0 sigma0 r' then
+      let sigma, c, c_eq = fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in
       let sigma, c_ty = Typing.type_of env sigma c in
         ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
       let open EConstr in
       match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
       | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
-          pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
+          pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, Tacticals.New.tclIDTAC, sigma0
       | _ ->
           let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in
           let sigma, _ = Typing.type_of env sigma cl' in
-          let gl = pf_merge_uc_of sigma gl in
-          Proofview.V82.of_tactic (convert_concl ~check:true cl'), rewritetac ?under dir r', gl
+          let sigma0 = pf_merge_uc_of sigma sigma0 in
+          convert_concl ~check:true cl', rewritetac ?under dir r', sigma0
     else
-      let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
+      let dc, r2 = EConstr.decompose_lam_n_assum sigma0 n r' in
       let r3, _, r3t  =
-        try EConstr.destCast (project gl) r2 with _ ->
-        errorstrm Pp.(str "no cast from " ++ pr_econstr_pat (pf_env gl) (project gl) (snd sr)
-                    ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in
+        try EConstr.destCast sigma0 r2 with _ ->
+        errorstrm Pp.(str "no cast from " ++ pr_econstr_pat env sigma0 (snd sr)
+                    ++ str " to " ++ pr_econstr_env env sigma0 r2) in
       let cl' = EConstr.mkNamedProd (make_annot rule_id Sorts.Relevant) (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in
       let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in
       let itacs = [introid pattern_id; introid rule_id] in
-      let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in
+      let cltac = Tactics.clear [pattern_id; rule_id] in
       let rwtacs = [rewritetac ?under dir (EConstr.mkVar rule_id); cltac] in
-      apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], tclTHENLIST (itacs @ rwtacs), gl
+      Tactics.apply_type ~typecheck:true cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), sigma0
   in
-  let cvtac' _ =
-    try cvtac gl with
-    | PRtype_error e ->
+  let cvtac' =
+    Proofview.tclOR cvtac begin function
+    | (PRtype_error e, _) ->
       let error = Option.cata (fun (env, sigma, te) ->
           Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te))
           (Pp.mt ()) e in
-      if occur_existential (project gl) (Tacmach.pf_concl gl)
-      then errorstrm Pp.(str "Rewriting impacts evars" ++ error)
-      else errorstrm Pp.(str "Dependent type error in rewrite of "
-        ++ pr_econstr_env (pf_env gl) (project gl)
+      if occur_existential sigma0 (Tacmach.New.pf_concl gl)
+      then Tacticals.New.tclZEROMSG Pp.(str "Rewriting impacts evars" ++ error)
+      else Tacticals.New.tclZEROMSG Pp.(str "Dependent type error in rewrite of "
+        ++ pr_econstr_env env sigma0
           (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl)
         ++ error)
+    | (e, info) -> Proofview.tclZERO ~info e
+    end
   in
-  tclTHEN cvtac' rwtac gl
+  Proofview.Unsafe.tclEVARS sigma0 <*>
+  Tacticals.New.tclTHEN cvtac' rwtac
+  end
 
 [@@@ocaml.warning "-3"]
 let lz_coq_prod =
@@ -474,14 +503,13 @@ let ssr_is_setoid env =
     Rewrite.is_applied_rewrite_relation env
       sigma [] (EConstr.mkApp (r, args)) <> None
 
-let closed0_check cl p gl =
+let closed0_check env sigma cl p =
   if closed0 cl then
-    errorstrm Pp.(str"No occurrence of redex "++ pr_constr_env (pf_env gl) (project gl) p)
+    errorstrm Pp.(str"No occurrence of redex "++ pr_constr_env env sigma p)
 
 let dir_org = function L2R -> 1 | R2L -> 2
 
-let rwprocess_rule dir rule gl =
-  let env = pf_env gl in
+let rwprocess_rule env dir rule =
   let coq_prod = lz_coq_prod () in
   let is_setoid = ssr_is_setoid env in
   let r_sigma, rules =
@@ -558,15 +586,17 @@ let rwprocess_rule dir rule gl =
   in
     r_sigma, rules
 
-let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl =
-  let env = pf_env gl in
-  let r_sigma, rules = rwprocess_rule dir rule gl in
+let rwrxtac ?under ?map_redex occ rdx_pat dir rule =
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma0 = Proofview.Goal.sigma gl in
+  let r_sigma, rules = rwprocess_rule env dir rule in
   let find_rule rdx =
     let rec rwtac = function
       | [] ->
-        errorstrm Pp.(str "pattern " ++ pr_econstr_pat env (project gl) rdx ++
+        errorstrm Pp.(str "pattern " ++ pr_econstr_pat env sigma0 rdx ++
                    str " does not match " ++ pr_dir_side dir ++
-                   str " of " ++ pr_econstr_pat env (project gl) (snd rule))
+                   str " of " ++ pr_econstr_pat env sigma0 (snd rule))
       | (d, r, lhs, rhs) :: rs ->
         try
           let ise = unify_HO env (Evd.create_evar_defs r_sigma) lhs rdx in
@@ -574,7 +604,8 @@ let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl =
           d, (ise, Evd.evar_universe_context ise, Reductionops.nf_evar ise r)
         with _ -> rwtac rs in
      rwtac rules in
-  let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
+  let env0 = env in
+  let concl0 = Proofview.Goal.concl gl in
   let find_R, conclude = match rdx_pat with
   | Some (_, (In_T _ | In_X_In_T _)) | None ->
       let upats_origin = dir, EConstr.Unsafe.to_constr (snd rule) in
@@ -586,23 +617,26 @@ let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl =
       let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
       let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in
       (fun e c _ i -> find_R ~k:(fun _ _ _ h -> mkRel h) e c i),
-      fun cl -> let rdx,d,r = end_R () in closed0_check cl rdx gl; (d,r),rdx
+      fun cl -> let rdx,d,r = end_R () in closed0_check env0 sigma0 cl rdx; (d,r),rdx
   | Some(_, (T e | X_In_T (_,e) | E_As_X_In_T (e,_,_) | E_In_X_In_T (e,_,_))) ->
       let r = ref None in
       (fun env c _ h -> do_once r (fun () -> find_rule (EConstr.of_constr c), c); mkRel h),
-      (fun concl -> closed0_check concl e gl;
+      (fun concl -> closed0_check env0 sigma0 concl e;
         let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ~abort_on_undefined_evars:false ev c)) , x) in
-  let concl0 = EConstr.Unsafe.to_constr concl0 in
+  let concl0 = EConstr.to_constr ~abort_on_undefined_evars:false sigma0 concl0 in
   let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in
   let (d, r), rdx = conclude concl in
   let r = Evd.merge_universe_context (pi1 r) (pi2 r), EConstr.of_constr (pi3 r) in
-  rwcltac ?under ?map_redex (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
-;;
-
-let ssrinstancesofrule ist dir arg 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
+  rwcltac ?under ?map_redex (EConstr.of_constr concl) (EConstr.of_constr rdx) d r
+  end
+
+let ssrinstancesofrule ist dir arg =
+  Proofview.Goal.enter begin fun gl ->
+  let env0 = Proofview.Goal.env gl in
+  let sigma0 = Proofview.Goal.sigma gl in
+  let concl0 = Proofview.Goal.concl gl in
+  let rule = interp_term env0 sigma0 ist arg in
+  let r_sigma, rules = rwprocess_rule env0 dir rule in
   let find, conclude =
     let upats_origin = dir, EConstr.Unsafe.to_constr (snd rule) in
     let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
@@ -619,33 +653,47 @@ let ssrinstancesofrule ist dir arg gl =
   Feedback.msg_info Pp.(str"BEGIN INSTANCES");
   try
     while true do
-      ignore(find env0 (EConstr.Unsafe.to_constr concl0) 1 ~k:print)
+      ignore(find env0 (EConstr.to_constr ~abort_on_undefined_evars:false sigma0 concl0) 1 ~k:print)
     done; raise NoMatch
-  with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); tclIDTAC gl
-
-let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl
-
-let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
+  with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); Tacticals.New.tclIDTAC
+  end
+
+let ipat_rewrite occ dir c = Proofview.Goal.enter begin fun gl ->
+  rwrxtac occ None dir (Proofview.Goal.sigma gl, c)
+end
+
+let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) =
+  let open Proofview.Notations in
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
   let fail = ref false in
-  let interp_rpattern gl gc =
-    try interp_rpattern gl gc
-    with _ when snd mult = May -> fail := true; project gl, T mkProp in
-  let interp gc gl =
-    try interp_term ist gl gc
-    with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in
-  let rwtac gl =
-    let rx = Option.map (interp_rpattern gl) grx in
-    let gl = match rx with
-      | None -> gl
-      | Some (s,_) -> pf_merge_uc_of s gl in
-    let t = interp gt gl in
-    let gl = pf_merge_uc_of (fst t) gl in
+  let interp_rpattern env sigma gc =
+    try interp_rpattern env sigma gc
+    with _ when snd mult = May -> fail := true; sigma, T mkProp in
+  let interp env sigma gc =
+    try interp_term env sigma ist gc
+    with _ when snd mult = May -> fail := true; (sigma, EConstr.mkProp) in
+  let rwtac =
+    Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let rx = Option.map (interp_rpattern env sigma) grx in
+    let sigma = match rx with
+      | None -> sigma
+      | Some (s,_) -> pf_merge_uc_of s sigma in
+    let t = interp env sigma gt in
+    let sigma = pf_merge_uc_of (fst t) sigma in
+    Proofview.Unsafe.tclEVARS sigma <*>
     (match kind with
     | RWred sim -> simplintac occ rx sim
     | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt
-    | RWeq -> rwrxtac ?under ?map_redex occ rx dir t) gl in
-  let ctac = old_cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in
-  if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl
+    | RWeq -> rwrxtac ?under ?map_redex occ rx dir t)
+    end
+  in
+  let ctac = cleartac (interp_clr sigma (oclr, (fst gt, snd (interp env sigma gt)))) in
+  if !fail then ctac else Tacticals.New.tclTHEN (tclMULT mult rwtac) ctac
+  end
 
 (** Rewrite argument sequence *)
 
@@ -654,24 +702,37 @@ 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.Goal.enter begin fun _ ->
+  Tacticals.New.tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs)
+  end
 
 (** The "unlock" tactic *)
 
-let unfoldtac occ ko t kt gl =
-  let env = pf_env gl in
-  let cl, c = pf_fill_occ_term gl occ (fst (strip_unfold_term env t kt)) in
-  let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref env (project gl) c] gl c) cl in
+let unfoldtac occ ko t kt =
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let concl = Proofview.Goal.concl gl in
+  let concl = Evarutil.nf_evar sigma concl in
+  let cl, c = fill_occ_term env sigma concl occ (fst (strip_unfold_term env t kt)) in
+  let cl' = EConstr.Vars.subst1 (Tacred.unfoldn [OnlyOccurrences [1], get_evalref env sigma c] env sigma c) cl in
   let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in
-  Proofview.V82.of_tactic
-    (convert_concl ~check:true (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl
-
-let unlocktac ist args 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
-  let key, gl = pf_mkSsrConst "master_key" gl in
+  convert_concl ~check:true (Reductionops.clos_norm_flags f env sigma cl')
+  end
+
+let unlocktac ist args =
+  let open Proofview.Notations in
+  let utac (occ, gt) =
+    Proofview.Goal.enter begin fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      unfoldtac occ occ (interp_term env sigma ist gt) (fst gt)
+    end
+  in
+  Ssrcommon.tacMK_SSR_CONST "locked" >>= fun locked ->
+  Ssrcommon.tacMK_SSR_CONST "master_key" >>= fun key ->
   let ktacs = [
-    (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
+    (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) xInParens);
+    Ssrelim.casetac key (fun ?seed:_ k -> k)
+  ] in
+  Tacticals.New.tclTHENLIST (List.map utac args @ ktacs)
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index 0bb67c99db..1c3b1bb018 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -26,12 +26,12 @@ val mkclr : ssrclear -> ssrdocc
 val nodocc : ssrdocc
 val noclr : ssrdocc
 
-val simpltac : Ssrast.ssrsimpl -> Tacmach.tactic
+val simpltac : Ssrast.ssrsimpl -> unit Proofview.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 ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> unit Proofview.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..4961138190 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -28,19 +28,22 @@ 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
-  let pat = interp_cpattern gl pat pty in
+  let pat = interp_cpattern (pf_env gl) (project gl) pat pty in
   let cl, sigma, env = pf_concl gl, project gl, pf_env gl in
   let (c, ucst), cl =
     let cl = EConstr.Unsafe.to_constr cl in
@@ -56,7 +59,8 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
   | Cast(t, DEFAULTcast, ty) -> t, (gl, ty)
   | _ -> 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
+  Proofview.V82.of_tactic (Tacticals.New.tclTHEN (convert_concl ~check:true cl') (introid id)) gl
+  end
 
 open Util
 
@@ -85,18 +89,30 @@ let combineCG t1 t2 f g = match t1, t2 with
  | _, (_, (_, None)) -> anomaly "have: mixed C-G constr"
  | _ -> anomaly "have: mixed G-C constr"
 
-let basecuttac name c gl =
-  let hd, gl = pf_mkSsrConst name gl in
-  let t = EConstr.mkApp (hd, [|c|]) in
-  let gl, _ = pf_e_type_of gl t in
-  Proofview.V82.of_tactic (Tactics.apply t) gl
+let basecuttac name t =
+  let open Proofview.Notations in
+  Ssrcommon.tacMK_SSR_CONST name >>= fun hd ->
+  let t = EConstr.mkApp (hd, [|t|]) in
+  Ssrcommon.tacTYPEOF t >>= fun _ty ->
+  Tactics.apply t
 
-let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats)
+let evarcuttac name cs =
+  let open Proofview.Notations in
+  Ssrcommon.tacMK_SSR_CONST name >>= fun hd ->
+  let t = EConstr.mkApp (hd, cs) in
+  Ssrcommon.tacTYPEOF t >>= fun _ty ->
+  applyn ~with_evars:true ~with_shelve:false (Array.length cs) t
+
+let introstac ipats = tclIPAT ipats
 
 let havetac ist
   (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint)))
-  suff namefst gl
+  suff namefst
 =
+ let open Proofview.Notations in
+ Ssrcommon.tacMK_SSR_CONST "abstract_key" >>= fun abstract_key ->
+ Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract ->
+ Proofview.V82.tactic begin fun gl ->
  let concl = pf_concl gl in
  let pats = tclCompileIPats orig_pats in
  let binders = tclCompileIPats binders in
@@ -108,34 +124,30 @@ let havetac ist
    match clr with
    | None -> introstac pats, []
    | Some clr -> introstac (tclCompileIPats (IPatClear clr :: orig_pats)), clr in
- let itac, id, clr = introstac pats, Tacticals.tclIDTAC, old_cleartac clr in
+ let itac, id, clr = introstac pats, Tacticals.New.tclIDTAC, cleartac clr in
  let binderstac n =
    let rec aux = function 0 -> [] | n -> IOpInaccessible None :: aux (n-1) in
-   Tacticals.tclTHEN (if binders <> [] then introstac (aux n) else Tacticals.tclIDTAC)
+   Tacticals.New.tclTHEN (if binders <> [] then introstac (aux n) else Tacticals.New.tclIDTAC)
      (introstac binders) in
  let simpltac = introstac simpl in
  let fixtc =
    not !ssrhaveNOtcresolution &&
    match fk with FwdHint(_,true) -> false | _ -> true in
  let hint = hinttac ist true hint in
- let cuttac t gl =
-   if transp then
-     let have_let, gl = pf_mkSsrConst "ssr_have_let" gl in
-     let step = EConstr.mkApp (have_let, [|concl;t|]) in
-     let gl, _ = pf_e_type_of gl step in
-     applyn ~with_evars:true ~with_shelve:false 2 step gl
-   else basecuttac "ssr_have" t gl in
+ let cuttac t = Proofview.Goal.enter begin fun gl ->
+   if transp then evarcuttac "ssr_have_let" [|concl;t|]
+   else basecuttac "ssr_have" t
+  end in
  (* Introduce now abstract constants, so that everything sees them *)
- let abstract_key, gl = pf_mkSsrConst "abstract_key" gl in
  let unlock_abs (idty,args_id) gl =
     let gl, _ = pf_e_type_of gl idty in
     pf_unify_HO gl args_id.(2) abstract_key in
- Tacticals.tclTHENFIRST itac_mkabs (fun gl ->
+ Tacticals.tclTHENFIRST (Proofview.V82.of_tactic itac_mkabs) (fun gl ->
   let mkt t = mk_term xNoFlag t in
   let mkl t = (xNoFlag, (t, None)) in
   let interp gl rtc t = pf_abs_ssrterm ~resolve_typeclasses:rtc ist gl t in
   let interp_ty gl rtc t =
-    let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc ist gl t in a,b,u in
+    let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc (pf_env gl) (project gl) ist t in a,b,u in
   let open CAst in
   let ct, cty, hole, loc = match Ssrcommon.ssrterm_of_ast_closure_term t with
     | _, (_, Some { loc; v = CCast (ct, CastConv cty)}) ->
@@ -163,7 +175,7 @@ let havetac ist
        try Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.it_mkProd_or_LetIn concl ctx)) gl
        with _ -> errorstrm (str "Given proof term is not of type " ++
          pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) Sorts.Relevant concl)) in
-     gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c
+     gl, ty, Tacticals.New.tclTHEN (Proofview.V82.tactic assert_is_conv) (Tactics.apply t), id, itac_c
    | FwdHave, false, false ->
      let skols = List.flatten (List.map (function
        | IOpAbstractVars ids -> ids
@@ -181,13 +193,12 @@ let havetac ist
      let gs =
        List.map (fun (_,a) ->
          Ssripats.Internal.pf_find_abstract_proof false gl (EConstr.Unsafe.to_constr a.(1))) skols_args in
-     let tacopen_skols gl = re_sig (gs @ [gl.Evd.it]) gl.Evd.sigma in
+     let tacopen_skols = Proofview.V82.tactic (fun gl -> re_sig (gs @ [gl.Evd.it]) gl.Evd.sigma) in
      let gl, ty = pf_e_type_of gl t in
-     gl, ty, Proofview.V82.of_tactic (Tactics.apply t), id,
-       Tacticals.tclTHEN (Tacticals.tclTHEN itac_c simpltac)
-         (Tacticals.tclTHEN tacopen_skols (fun gl ->
-            let abstract, gl = pf_mkSsrConst "abstract" gl in
-            Proofview.V82.of_tactic (unfold [abstract; abstract_key]) gl))
+     gl, ty, Tactics.apply t, id,
+       Tacticals.New.tclTHEN (Tacticals.New.tclTHEN itac_c simpltac)
+         (Tacticals.New.tclTHEN tacopen_skols (Proofview.V82.tactic (fun gl ->
+            Proofview.V82.of_tactic (unfold [abstract; abstract_key]) gl)))
    | _,true,true  ->
      let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in
      gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, itac, clr
@@ -196,11 +207,11 @@ let havetac ist
      gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, id, itac_c
    | _, false, false ->
      let n, cty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in
-     gl, cty, Tacticals.tclTHEN (binderstac n) hint, id, Tacticals.tclTHEN itac_c simpltac
+     gl, cty, Tacticals.New.tclTHEN (binderstac n) hint, id, Tacticals.New.tclTHEN itac_c simpltac
    | _, true, false -> assert false in
-  Tacticals.tclTHENS (cuttac cut) [ Tacticals.tclTHEN sol itac1; itac2 ] gl)
+  Proofview.V82.of_tactic (Tacticals.New.tclTHENS (cuttac cut) [ Tacticals.New.tclTHEN sol itac1; itac2 ]) gl)
  gl
-;;
+end
 
 let destProd_or_LetIn sigma c =
   match EConstr.kind sigma c with
@@ -208,7 +219,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
@@ -243,7 +255,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
     let (sigma, ev) = Evarutil.new_evar env sigma EConstr.mkProp in
     let k, _ = EConstr.destEvar sigma ev in
     let fake_gl = {Evd.it = k; Evd.sigma = sigma} in
-    let _, ct, _, uc = pf_interp_ty ist fake_gl ct in
+    let _, ct, _, uc = pf_interp_ty (pf_env fake_gl) sigma ist ct in
     let rec var2rel c g s = match EConstr.kind sigma c, g with
       | Prod({binder_name=Anonymous} as x,_,c), [] -> EConstr.mkProd(x, EConstr.Vars.subst_vars s ct, c)
       | Sort _, [] -> EConstr.Vars.subst_vars s ct
@@ -260,39 +272,40 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
     c, args, pired c args, pf_merge_uc uc gl in
   let tacipat pats = introstac pats in
   let tacigens =
-    Tacticals.tclTHEN
-      (Tacticals.tclTHENLIST(List.rev(List.fold_right mkclr gens [old_cleartac clr0])))
+    Tacticals.New.tclTHEN
+      (Tacticals.New.tclTHENLIST(List.rev(List.fold_right mkclr gens [cleartac clr0])))
       (introstac (List.fold_right mkpats gens [])) in
   let hinttac = 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
-    | false, `NoGen -> "ssr_wlog", hinttac, Tacticals.tclTHEN tacigens (tacipat pats)
+    | true, `NoGen -> "ssr_wlog", Tacticals.New.tclTHEN hinttac (tacipat pats), tacigens
+    | false, `NoGen -> "ssr_wlog", hinttac, Tacticals.New.tclTHEN tacigens (tacipat pats)
     | true, `Gen _ -> assert false
     | false, `Gen id ->
       if gens = [] then errorstrm(str"gen have requires some generalizations");
-      let clear0 = old_cleartac clr0 in
+      let clear0 = cleartac clr0 in
       let id, name_general_hyp, cleanup, pats = match id, pats with
       | None, (IOpId id as ip)::pats -> Some id, tacipat [ip], clear0, pats
-      | None, _ -> None, Tacticals.tclIDTAC, clear0, pats
+      | None, _ -> None, Tacticals.New.tclIDTAC, clear0, pats
       | Some (Some id),_ -> Some id, introid id, clear0, pats
       | Some _,_ ->
           let id = mk_anon_id "tmp" (Tacmach.pf_ids_of_hyps gl) in
-          Some id, introid id, Tacticals.tclTHEN clear0 (Proofview.V82.of_tactic (Tactics.clear [id])), pats in
+          Some id, introid id, Tacticals.New.tclTHEN clear0 (Tactics.clear [id]), pats in
       let tac_specialize = match id with
-      | None -> Tacticals.tclIDTAC
+      | None -> Tacticals.New.tclIDTAC
       | Some id ->
-        if pats = [] then Tacticals.tclIDTAC else
+        if pats = [] then Tacticals.New.tclIDTAC else
         let args = Array.of_list args in
         ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args))));
         ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct));
-        Tacticals.tclTHENS (basecuttac "ssr_have" ct)
-          [Proofview.V82.of_tactic (Tactics.apply EConstr.(mkApp (mkVar id,args))); Tacticals.tclIDTAC] in
+        Tacticals.New.tclTHENS (basecuttac "ssr_have" ct)
+          [Tactics.apply EConstr.(mkApp (mkVar id,args)); Tacticals.New.tclIDTAC] in
       "ssr_have",
       (if hint = nohint then tacigens else hinttac),
-      Tacticals.tclTHENLIST [name_general_hyp; tac_specialize; tacipat pats; cleanup]
+      Tacticals.New.tclTHENLIST [name_general_hyp; tac_specialize; tacipat pats; cleanup]
   in
-  Tacticals.tclTHENS (basecuttac cut_kind c) [fst_goal_tac; snd_goal_tac] gl
+  Proofview.V82.of_tactic (Tacticals.New.tclTHENS (basecuttac cut_kind c) [fst_goal_tac; snd_goal_tac]) gl
+  end
 
 (** The "suffice" tactic *)
 
@@ -301,7 +314,7 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
   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.New.tclTHEN (introstac pats) (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
@@ -314,10 +327,12 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
     | _ -> anomaly "suff: ssr cast hole deleted by typecheck"
     end
   in
-  let ctac gl =
-    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))]
+  let ctac =
+    Proofview.V82.tactic begin fun gl ->
+    let _,ty,_,uc = pf_interp_ty (pf_env gl) (project gl) ist c in let gl = pf_merge_uc uc gl in
+    Proofview.V82.of_tactic (basecuttac "ssr_suff" ty) gl
+  end in
+  Tacticals.New.tclTHENS ctac [htac; Tacticals.New.tclTHEN (cleartac clr) (introstac (binders@simpl))]
 
 open Proofview.Notations
 
@@ -340,16 +355,14 @@ let intro_lock ipats =
              Proofview.tclDISPATCH
                (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in
   let protect_subgoal env sigma hd args =
+    Ssrcommon.tacMK_SSR_CONST "Under_rel" >>= fun under_rel ->
+    Ssrcommon.tacMK_SSR_CONST "Under_rel_from_rel" >>= fun under_from_rel ->
     Tactics.New.refine ~typecheck:true (fun sigma ->
         let lm2 = Array.length args - 2 in
         let sigma, carrier =
           Typing.type_of env sigma args.(lm2) in
         let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in
         let rel_args = Array.sub args lm2 2 in
-        let sigma, under_rel =
-          Ssrcommon.mkSsrConst "Under_rel" env sigma in
-        let sigma, under_from_rel =
-          Ssrcommon.mkSsrConst "Under_rel_from_rel" env sigma in
         let under_rel_args = Array.append [|carrier; rel|] rel_args in
         let ty = EConstr.mkApp (under_rel, under_rel_args) in
         let sigma, t = Evarutil.new_evar env sigma ty in
@@ -408,7 +421,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 +505,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..33bf56cfa9 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,11 +27,9 @@ 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 ->
-           EConstr.t -> Goal.goal Evd.sigma -> Evar.t list Evd.sigma
+val basecuttac : string -> EConstr.t -> unit Proofview.tactic
 
 val wlogtac :
   Ltac_plugin.Tacinterp.interp_sign ->
@@ -46,7 +44,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 +53,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..46f90a7ee1 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -191,7 +191,7 @@ let isGEN_PUSH dg =
 (* generalize `id` as `new_name` *)
 let gen_astac id new_name =
  let gen = ((None,Some(false,[])),Ssrmatching.cpattern_of_id id) in
- V82.tactic (Ssrcommon.gentac gen)
+ Ssrcommon.gentac gen
  <*> Ssrcommon.tclRENAME_HD_PROD new_name
 
 (* performs and resets all delayed generalizations *)
@@ -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 ->
@@ -384,13 +384,11 @@ end
 
 let tclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
   let env, concl = Goal.(env gl, concl gl) in
-  let step = begin fun sigma ->
+  let step ablock abstract = begin fun sigma ->
     let (sigma, (abstract_proof, abstract_ty)) =
       let (sigma, (ty, _)) =
         Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in
-      let (sigma, ablock) = Ssrcommon.mkSsrConst "abstract_lock" env sigma in
       let (sigma, lock) = Evarutil.new_evar env sigma ablock in
-      let (sigma, abstract) = Ssrcommon.mkSsrConst "abstract" env sigma in
       let (sigma, abstract_id) = mk_abstract_id env sigma in
       let abstract_ty = EConstr.mkApp(abstract, [|ty; abstract_id; lock|]) in
       let sigma, m = Evarutil.new_evar env sigma abstract_ty in
@@ -405,7 +403,9 @@ let tclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
     let sigma, _ = Typing.type_of env sigma term in
     sigma, term
   end in
-  Tactics.New.refine ~typecheck:false step <*>
+  Ssrcommon.tacMK_SSR_CONST "abstract_lock" >>= fun ablock ->
+  Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract ->
+  Tactics.New.refine ~typecheck:false (step ablock abstract) <*>
   tclFOCUS 1 3 Proofview.shelve
 end
 
@@ -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
 
@@ -494,11 +494,11 @@ let rec ipat_tac1 ipat : bool tactic =
       notTAC
 
   | IOpSimpl x ->
-      V82.tactic ~nf_evars:false (Ssrequality.simpltac x) <*> notTAC
+      Ssrequality.simpltac x <*> notTAC
 
   | IOpRewrite (occ,dir) ->
      Ssrcommon.tclWITHTOP
-       (fun x -> V82.tactic  ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x)) <*> notTAC
+       (fun x -> Ssrequality.ipat_rewrite occ dir x) <*> notTAC
 
   | IOpAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> 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 <*>
@@ -727,7 +727,7 @@ let mkEq dir cl c t n env sigma =
 let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
   Ssrcommon.tacSIGMA >>= fun sigma0 ->
   Goal.enter_one begin fun g ->
-  let pat = Ssrmatching.interp_cpattern sigma0 t None in
+  let pat = Ssrmatching.interp_cpattern (Tacmach.pf_env sigma0) (Tacmach.project sigma0) t None in
   let cl0, env, sigma, hyps = Goal.(concl g, env g, sigma g, hyps g) in
   let cl = EConstr.to_constr ~abort_on_undefined_evars:false sigma cl0 in
   let (c, ucst), cl =
@@ -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)]
@@ -985,7 +985,7 @@ let ssrabstract dgens =
    Ssrcommon.tacSIGMA >>= fun gl0 ->
      let open Ssrmatching in
      let ipats = List.map (fun (_,cp) ->
-       match id_of_pattern (interp_cpattern gl0 cp None) with
+       match id_of_pattern (interp_cpattern (Tacmach.pf_env gl0) (Tacmach.project gl0) cp None) with
        | None -> IPatAnon (One None)
        | Some id -> IPatId id)
        (List.tl gens) in
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..cbc352126e 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -30,10 +30,12 @@ let get_index = function Locus.ArgArg i -> i | _ ->
 
 (** The "first" and "last" tacticals. *)
 
-let tclPERM perm tac gls =
-  let subgls = tac gls in
+let tclPERM perm tac =
+  Proofview.V82.tactic begin fun gls ->
+  let subgls = Proofview.V82.of_tactic tac gls in
   let subgll' = perm subgls.Evd.it in
   re_sig subgll' subgls.Evd.sigma
+  end
 
 let rot_hyps dir i hyps =
   let n = List.length hyps in
@@ -46,17 +48,17 @@ let rot_hyps dir i hyps =
 
 let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) =
   let i = get_index ivar in
-  let evtac t = Proofview.V82.of_tactic (ssrevaltac ist t) in
+  let evtac t = ssrevaltac ist t in
   let tac1 = evtac atac1 in
   if atacs2 = [] && atac3 <> None then tclPERM (rot_hyps dir i) tac1  else
-  let evotac = function Some atac -> evtac atac | _ -> Tacticals.tclIDTAC in
+  let evotac = function Some atac -> evtac atac | _ -> Tacticals.New.tclIDTAC in
   let tac3 = evotac atac3 in
   let rec mk_pad n = if n > 0 then tac3 :: mk_pad (n - 1) else [] in
   match dir, mk_pad (i - 1), List.map evotac atacs2 with
-  | L2R, [], [tac2] when atac3 = None -> Tacticals.tclTHENFIRST tac1 tac2
-  | 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))
+  | L2R, [], [tac2] when atac3 = None -> Tacticals.New.tclTHENFIRST tac1 tac2
+  | L2R, [], [tac2] when atac3 = None -> Tacticals.New.tclTHENLAST tac1 tac2
+  | L2R, pad, tacs2 -> Tacticals.New.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3
+  | R2L, pad, tacs2 -> Tacticals.New.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad))
 
 (** The "in" pseudo-tactical *)(* {{{ **********************************************)
 
@@ -74,7 +76,7 @@ let check_wgen_uniq gens =
   | [] -> () in
   check [] ids
 
-let pf_clauseids gl gens clseq =
+let pf_clauseids gens clseq =
   let keep_clears = List.map (fun (x, _) -> x, None) in
   if gens <> [] then (check_wgen_uniq gens; gens) else
   if clseq <> InAll && clseq <> InAllHyps then keep_clears gens else
@@ -82,14 +84,15 @@ let pf_clauseids gl gens clseq =
 
 let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false
 
-let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl)
+let posetac id cl = Tactics.pose_tac (Name id) cl
 
 let hidetacs clseq idhide cl0 =
   if not (hidden_clseq clseq) then  [] else
   [posetac idhide cl0;
-   Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkVar idhide))]
+   convert_concl_no_check (EConstr.mkVar idhide)]
 
-let endclausestac id_map clseq gl_id cl0 gl =
+let endclausestac id_map clseq gl_id cl0 =
+  Proofview.V82.tactic begin fun gl ->
   let not_hyp' id = not (List.mem_assoc id id_map) in
   let orig_id id = try List.assoc id id_map with Not_found -> id in
   let dc, c = EConstr.decompose_prod_assum (project gl) (pf_concl gl) in
@@ -124,40 +127,45 @@ let endclausestac id_map clseq gl_id cl0 gl =
   let all_ids = ids_of_rel_context dc @ pf_ids_of_hyps gl in
   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 =
-  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
-  let gl_id = mk_anon_id hidden_goal_tag (Tacmach.pf_ids_of_hyps gl) in
-  let cl0 = pf_concl gl in
-  let dtac gl =
+  end
+
+let tclCLAUSES tac (gens, clseq) =
+  Proofview.Goal.enter begin fun gl ->
+  if clseq = InGoal || clseq = InSeqGoal then tac else
+  let clr_gens = pf_clauseids gens clseq in
+  let clear = Tacticals.New.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in
+  let gl_id = mk_anon_id hidden_goal_tag (Tacmach.New.pf_ids_of_hyps gl) in
+  let cl0 = Proofview.Goal.concl gl in
+  let dtac =
+    Proofview.V82.tactic begin fun gl ->
     let c = pf_concl gl in
     let gl, args, c =
       List.fold_right (abs_wgen true mk_discharged_id) gens (gl,[], c) in
-    apply_type c args gl in
+    apply_type c args gl
+    end
+  in
   let endtac =
     let id_map = CList.map_filter (function
       | _, Some ((x,_),_) -> let id = hoi_id x in Some (mk_discharged_id id, id)
       | _, None -> None) gens in
     endclausestac id_map clseq gl_id cl0 in
-  Tacticals.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; clear; tac; endtac]) gl
+  Tacticals.New.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; clear; tac; endtac])
+  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.Goal.enter begin fun _ ->
+  let dtac = if is_by then donetac ~-1 else Tacticals.New.tclIDTAC in
   let mktac = function
-  | Some atac -> Tacticals.tclTHEN (Proofview.V82.of_tactic (ssrevaltac ist atac)) dtac
+  | Some atac -> Tacticals.New.tclTHEN (ssrevaltac ist atac) dtac
   | _ -> dtac in
   match List.map mktac atacs with
-  | [] -> if is_or then dtac else Tacticals.tclIDTAC
+  | [] -> if is_or then dtac else Tacticals.New.tclIDTAC
   | [tac] -> tac
-  | tacs -> Tacticals.tclFIRST tacs
+  | tacs -> Tacticals.New.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))
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..adaf7c8cc1 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -14,7 +14,6 @@ open Ltac_plugin
 open Names
 open Pp
 open Genarg
-open Stdarg
 open Term
 open Context
 module CoqConstr = Constr
@@ -22,7 +21,6 @@ open CoqConstr
 open Vars
 open Libnames
 open Tactics
-open Tacticals
 open Termops
 open Recordops
 open Tacmach
@@ -173,8 +171,6 @@ let loc_ofCG = function
 let mk_term k c ist = k, (mkRHole, Some c), ist
 let mk_lterm = mk_term ' '
 
-let pf_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl)  sigma, ty
-
 let nf_evar sigma c =
   EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c))
 
@@ -932,31 +928,15 @@ let id_of_Cterm t = match id_of_cpattern t with
   | Some x -> x
   | None -> loc_error (loc_of_cpattern t) "Only identifiers are allowed here"
 
-let of_ftactic ftac gl =
-  let r = ref None in
-  let tac = Ftactic.run ftac (fun ans -> r := Some ans; Proofview.tclUNIT ()) in
-  let tac = Proofview.V82.of_tactic tac in
-  let { sigma = sigma } = tac gl in
-  let ans = match !r with
-  | None -> assert false (* If the tactic failed we should not reach this point *)
-  | Some ans -> ans
-  in
-  (sigma, ans)
-
-let interp_wit wit ist gl x =
-  let globarg = in_gen (glbwit wit) x in
-  let arg = interp_genarg ist globarg in
-  let (sigma, arg) = of_ftactic arg gl in
-  sigma, Value.cast (topwit wit) arg
-let interp_open_constr ist gl gc =
-  interp_wit wit_open_constr ist gl gc
-let pf_intern_term gl (_, c, ist) = glob_constr ist (pf_env gl) (project gl) c
+let interp_open_constr ist env sigma gc =
+  Tacinterp.interp_open_constr ist env sigma gc
+let pf_intern_term env sigma (_, c, ist) = glob_constr ist env sigma c
 
 let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t
 
-let interp_term gl = function
+let interp_term env sigma = function
   | (_, c, Some ist) ->
-      on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c)
+      on_snd EConstr.Unsafe.to_constr (interp_open_constr ist env sigma c)
   | _ -> errorstrm (str"interpreting a term with no ist")
 
 let thin id sigma goal =
@@ -982,7 +962,7 @@ let pr_ist { lfun= lfun } =
         pr_id id ++ str":" ++ Geninterp.Val.pr ty) (Id.Map.bindings lfun)
 *)
 
-let interp_pattern ?wit_ssrpatternarg gl red redty =
+let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
   pp(lazy(str"interpreting: " ++ pr_pattern red));
   let xInT x y = X_In_T(x,y) and inXInT x y = In_X_In_T(x,y) in
   let inT x = In_T x and eInXInT e x t = E_In_X_In_T(e,x,t) in
@@ -990,7 +970,7 @@ let interp_pattern ?wit_ssrpatternarg gl red redty =
   let mkG ?(k=' ') x ist = k,(x,None), ist in
   let ist_of (_,_,ist) = ist in
   let decode (_,_,ist as t) ?reccall f g =
-    try match DAst.get (pf_intern_term gl t) with
+    try match DAst.get (pf_intern_term env sigma0 t) with
     | GCast(t,CastConv c) when isGHole t && isGLambda c->
       let (x, c) = destGLambda c in
       f x (' ',(c,None),ist)
@@ -1008,7 +988,7 @@ let interp_pattern ?wit_ssrpatternarg gl red redty =
   let cleanup_XinE h x rp sigma =
     let h_k = match kind h with Evar (k,_) -> k | _ -> assert false in
     let to_clean, update = (* handle rename if x is already used *)
-      let ctx = pf_hyps gl in
+      let ctx = Environ.named_context env in
       let len = Context.Named.length ctx in
       let name = ref None in
       try ignore(Context.Named.lookup x ctx); (name, fun k ->
@@ -1019,7 +999,6 @@ let interp_pattern ?wit_ssrpatternarg gl red redty =
           name := Some (Context.Named.Declaration.get_id (List.nth nctx (nlen - len - 1)))
         end)
       with Not_found -> ref (Some x), fun _ -> () in
-    let sigma0 = project gl in
     let new_evars =
       let rec aux acc t = match kind t with
       | Evar (k,_) ->
@@ -1072,13 +1051,13 @@ let interp_pattern ?wit_ssrpatternarg gl red redty =
   match red with
   | T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast)
   | X_In_T (x,t) ->
-      let gty = pf_intern_term gl ty in
+      let gty = pf_intern_term env sigma0 ty in
       E_As_X_In_T (mkG (mkRCast mkRHole gty) (ist_of ty), x, t)
   | E_In_X_In_T (e,x,t) ->
-      let ty = mkG (pf_intern_term gl ty) (ist_of ty) in
+      let ty = mkG (pf_intern_term env sigma0 ty) (ist_of ty) in
       E_In_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t)
   | E_As_X_In_T (e,x,t) ->
-      let ty = mkG (pf_intern_term gl ty) (ist_of ty) in
+      let ty = mkG (pf_intern_term env sigma0 ty) (ist_of ty) in
       E_As_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t)
   | red -> red in
   pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
@@ -1086,12 +1065,12 @@ let interp_pattern ?wit_ssrpatternarg gl red redty =
   | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)), ist
   | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None), ist in
   match red with
-  | T t -> let sigma, t = interp_term gl t in sigma, T t
-  | In_T t -> let sigma, t = interp_term gl t in sigma, In_T t
+  | T t -> let sigma, t = interp_term env sigma0 t in sigma, T t
+  | In_T t -> let sigma, t = interp_term env sigma0 t in sigma, In_T t
   | X_In_T (x, rp) | In_X_In_T (x, rp) ->
     let mk x p = match red with X_In_T _ -> X_In_T(x,p) | _ -> In_X_In_T(x,p) in
     let rp = mkXLetIn (Name x) rp in
-    let sigma, rp = interp_term gl rp in
+    let sigma, rp = interp_term env sigma0 rp in
     let _, h, _, rp = destLetIn rp in
     let sigma = cleanup_XinE h x rp sigma in
     let rp = subst1 h (nf_evar sigma rp) in
@@ -1100,15 +1079,15 @@ let interp_pattern ?wit_ssrpatternarg gl red redty =
     let mk e x p =
       match red with E_In_X_In_T _ ->E_In_X_In_T(e,x,p)|_->E_As_X_In_T(e,x,p) in
     let rp = mkXLetIn (Name x) rp in
-    let sigma, rp = interp_term gl rp in
+    let sigma, rp = interp_term env sigma0 rp in
     let _, h, _, rp = destLetIn rp in
     let sigma = cleanup_XinE h x rp sigma in
     let rp = subst1 h (nf_evar sigma rp) in
-    let sigma, e = interp_term (re_sig (sig_it gl) sigma) e in
+    let sigma, e = interp_term env sigma e in
     sigma, mk e h rp
 ;;
-let interp_cpattern gl red redty = interp_pattern gl (T red) redty;;
-let interp_rpattern ~wit_ssrpatternarg gl red = interp_pattern ~wit_ssrpatternarg gl red None;;
+let interp_cpattern env sigma red redty = interp_pattern env sigma (T red) redty;;
+let interp_rpattern ~wit_ssrpatternarg env sigma red = interp_pattern ~wit_ssrpatternarg env sigma red None;;
 
 let id_of_pattern = function
   | _, T t -> (match kind t with Var id -> Some id | _ -> None)
@@ -1245,23 +1224,23 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h =
  let rdx, _, (sigma, uc, p) = end_U () in
  sigma, uc, EConstr.of_constr p, EConstr.of_constr concl, EConstr.of_constr rdx
 
-let fill_occ_term env cl occ sigma0 (sigma, t) =
+let fill_occ_term env sigma0 cl occ (sigma, t) =
   try
     let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in
     if sigma' != sigma0 then CErrors.user_err Pp.(str "matching impacts evars")
-    else cl, (Evd.merge_universe_context sigma' uc, t')
+    else cl, t'
   with NoMatch -> try
     let sigma', uc, t' =
       unif_end env sigma0 (create_evar_defs sigma) t (fun _ -> true) in
     if sigma' != sigma0 then raise NoMatch
-    else cl, (Evd.merge_universe_context sigma' uc, t')
+    else cl, t'
   with _ ->
     errorstrm (str "partial term " ++ pr_econstr_pat env sigma t
             ++ str " does not match any subterm of the goal")
 
 let pf_fill_occ_term gl occ t =
   let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in
-  let cl,(_,t) = fill_occ_term env concl occ sigma0 t in
+  let cl, t = fill_occ_term env sigma0 concl occ t in
   cl, t
 
 let cpattern_of_id id =
@@ -1286,18 +1265,23 @@ let wit_ssrpatternarg = wit_rpatternty
 
 let interp_rpattern = interp_rpattern ~wit_ssrpatternarg
 
-let ssrpatterntac _ist arg gl =
-  let pat = interp_rpattern gl arg in
-  let sigma0 = project gl in
-  let concl0 = pf_concl gl in
+let ssrpatterntac _ist arg =
+  let open Proofview.Notations in
+  Proofview.Goal.enter begin fun gl ->
+  let sigma0 = Proofview.Goal.sigma gl in
+  let concl0 = Proofview.Goal.concl gl in
+  let env = Proofview.Goal.env gl in
+  let pat = interp_rpattern env sigma0 arg in
   let concl0 = EConstr.Unsafe.to_constr concl0 in
   let (t, uc), concl_x =
-    fill_occ_pattern (pf_env gl) sigma0 concl0 pat noindex 1 in
+    fill_occ_pattern env sigma0 concl0 pat noindex 1 in
   let t = EConstr.of_constr t in
   let concl_x = EConstr.of_constr concl_x in
-  let gl, tty = pf_type_of gl t in
+  let sigma, tty = Typing.type_of env sigma0 t in
   let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in
-  Proofview.V82.of_tactic (convert_concl ~check:true concl DEFAULTcast) gl
+  Proofview.Unsafe.tclEVARS sigma <*>
+  convert_concl ~check:true concl DEFAULTcast
+  end
 
 (* Register "ssrpattern" tactic *)
 let () =
@@ -1305,7 +1289,7 @@ let () =
     let arg =
       let v = Id.Map.find (Names.Id.of_string "pattern") ist.lfun in
       Value.cast (topwit wit_ssrpatternarg) v in
-    Proofview.V82.tactic (ssrpatterntac ist arg) in
+    ssrpatterntac ist arg in
   let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in
   let () = Tacenv.register_ml_tactic name [|mltac|] in
   let tac =
@@ -1315,25 +1299,29 @@ 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.Goal.enter 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
-  let concl = EConstr.Unsafe.to_constr concl in
-  let sigma0, cpat = interp_cpattern gl arg None in
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let concl = Proofview.Goal.concl gl in
+  let concl = EConstr.to_constr ~abort_on_undefined_evars:false sigma concl in
+  let sigma0, cpat = interp_cpattern env sigma arg None in
   let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in
   let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in
   let find, conclude =
     mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true
       sigma None (etpat,[tpat]) in
-  let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) p ++ spc()
-                                     ++ str "matches:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma)  c)); c in
+  let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env env (Proofview.Goal.sigma gl) p ++ spc()
+                                     ++ str "matches:" ++ spc() ++ pr_constr_env env (Proofview.Goal.sigma gl)  c)); c in
   ppnl (str"BEGIN INSTANCES");
   try
     while true do
       ignore(find env concl 1 ~k:print)
     done; raise NoMatch
-  with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl
+  with NoMatch -> ppnl (str"END INSTANCES"); Tacticals.New.tclIDTAC
+  end
 
 module Internal =
 struct
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 31b414cc42..17b47227cb 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -57,7 +57,7 @@ val redex_of_pattern :
 (** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat]
     in the current [Ltac] interpretation signature [ise] and tactic input [gl]*)
 val interp_rpattern :
-  goal sigma ->
+  Environ.env -> Evd.evar_map ->
   rpattern ->
     pattern
 
@@ -65,7 +65,7 @@ val interp_rpattern :
     in the current [Ltac] interpretation signature [ise] and tactic input [gl].
     [ty] is an optional type for the redex of [cpat] *)
 val interp_cpattern :
-  goal sigma ->
+  Environ.env -> Evd.evar_map ->
   cpattern -> (glob_constr_and_expr * Geninterp.interp_sign) option ->
     pattern
 
@@ -191,6 +191,8 @@ val mk_tpattern_matcher :
  * by [Rel 1] and the instance of [t] *)
 val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t
 
+val fill_occ_term : Environ.env -> Evd.evar_map -> EConstr.t -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t
+
 (* It may be handy to inject a simple term into the first form of cpattern *)
 val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> cpattern
 
@@ -230,7 +232,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. *)
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 767f93787d..695e103082 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -61,10 +61,7 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv =
   clenv_pose_metas_as_evars clenv dep_mvs
 
 let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
-  (* ppedrot: a Goal.enter here breaks things, because the tactic below may
-     solve goals by side effects, while the compatibility layer keeps those
-     useless goals. That deserves a FIXME. *)
-  Proofview.V82.tactic begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in
   let evd' =
     if with_classes then
@@ -78,9 +75,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
-  tclTHEN
-    (tclEVARS (Evd.clear_metas evd'))
-    (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl
+  Proofview.tclTHEN
+    (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd'))
+    (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))
   end
 
 let clenv_pose_dependent_evars ?(with_evars=false) clenv =
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 75c3436cf4..29a47c5acd 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -37,6 +37,8 @@ let refiner ~check =
       CProfile.profile2 refiner_key (refiner ~check)
   else refiner ~check
 
+let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c)
+
 (*********************)
 (*   Tacticals       *)
 (*********************)
@@ -269,5 +271,3 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
 
 (* Change evars *)
 let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
-let tclPUSHEVARUNIVCONTEXT ctx gl =
-  tclEVARS (Evd.merge_universe_context (project gl) ctx) gl
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 66eae1db81..3471f38e9e 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -22,7 +22,7 @@ val project : 'a sigma -> evar_map
 val pf_env  : Goal.goal sigma -> Environ.env
 val pf_hyps : Goal.goal sigma -> named_context
 
-val refiner : check:bool -> Constr.t -> tactic
+val refiner : check:bool -> Constr.t -> unit Proofview.tactic
 
 (** {6 Tacticals. } *)
 
@@ -32,7 +32,6 @@ val tclIDTAC_MESSAGE  : Pp.t -> tactic
 
 (** [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
-val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic
 
 
 (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
diff --git a/stm/stm.ml b/stm/stm.ml
index f3768e9b99..5790bfc07e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2023,12 +2023,16 @@ end = struct (* {{{ *)
           match Future.join f with
           | Some (pt, uc) ->
             let sigma, env = PG_compat.get_current_context () in
+            let push_state ctx =
+              Proofview.tclEVARMAP >>= fun sigma ->
+              Proofview.Unsafe.tclEVARS (Evd.merge_universe_context sigma ctx)
+            in
             stm_pperr_endline (fun () -> hov 0 (
               str"g=" ++ int (Evar.repr gid) ++ spc () ++
               str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++
               str"uc=" ++ Termops.pr_evar_universe_context uc));
             (if abstract then Abstract.tclABSTRACT None else (fun x -> x))
-              (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
+              (push_state uc <*>
               Tactics.exact_no_check (EConstr.of_constr pt))
           | None ->
             if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f3073acb0a..e1d34af13e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1043,7 +1043,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
     let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
     let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
     tclTHENS (assert_after Anonymous false_0)
-      [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))]
+      [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))]
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
@@ -1360,8 +1360,8 @@ let inject_if_homogenous_dependent_pair ty =
         tclTHENS (cut (mkApp (ceq,new_eq_args)))
           [clear [destVar sigma hyp];
            Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 ->
-           Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr
-             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
+           Refiner.refiner ~check:true EConstr.Unsafe.(to_constr
+             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
           ])]
   with Exit ->
     Proofview.tclUNIT ()
@@ -1406,7 +1406,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       (Proofview.tclIGNORE (Proofview.Monad.List.map
          (fun (pf,ty) -> tclTHENS (cut ty)
            [inject_if_homogenous_dependent_pair ty;
-            Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))])
+            Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)])
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 8f6844079b..07f9def2c8 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -368,6 +368,9 @@ module New = struct
     Proofview.Unsafe.tclNEWGOALS tl <*>
     Proofview.tclUNIT ans
 
+  let tclTHENSLASTn t1 repeat l =
+    tclTHENS3PARTS t1 [||] repeat l
+
   let tclTHENLASTn t1 l =
     tclTHENS3PARTS t1 [||] (tclUNIT()) l
   let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|]
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 9ec558f1ad..01565169ca 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -180,6 +180,7 @@ module New : sig
       middle. Raises an error if the number of resulting subgoals is
       strictly less than [n+m] *)
   val tclTHENS3PARTS     : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic
+  val tclTHENSLASTn    : unit tactic -> unit tactic -> unit tactic array -> unit tactic
   val tclTHENSFIRSTn : unit tactic -> unit tactic array -> unit tactic -> unit tactic
   val tclTHENFIRSTn : unit tactic -> unit tactic array -> unit tactic
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0df4f5b207..e4809332c5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1368,7 +1368,7 @@ let clenv_refine_in with_evars targetid id sigma0 clenv tac =
   if not with_evars && occur_meta clenv.evd new_hyp_typ then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
-  let exact_tac = Proofview.V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf)) in
+  let exact_tac = Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in
   let naming = NamingMustBe (CAst.make targetid) in
   let with_clear = do_replace (Some id) naming in
   Tacticals.New.tclTHEN
@@ -1670,7 +1670,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
             | Some (p,pt) ->
               Tacticals.New.tclTHENS
                 (assert_before_gen false (NamingAvoid avoid) pt)
-                [Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p));
+                [refiner ~check:true EConstr.Unsafe.(to_constr p);
                  (* Might be ill-typed due to forbidden elimination. *)
                  Tacticals.New.onLastHypId (tac (not isrec))]
            end)))
diff --git a/test-suite/ssr/simpl_done.v b/test-suite/ssr/simpl_done.v
new file mode 100644
index 0000000000..f5c766209a
--- /dev/null
+++ b/test-suite/ssr/simpl_done.v
@@ -0,0 +1,28 @@
+Require Import ssreflect.
+
+Inductive lit : Set :=
+| LitP : lit
+| LitL : lit
+.
+
+Inductive val : Set :=
+| Val : lit -> val.
+
+Definition tyref :=
+fun (vl : list val) =>
+match vl with
+| cons (Val LitL) (cons (Val LitP) _)  => False
+| _ => False
+end.
+
+(** Check that simplification and resolution are performed in the right order
+    by "//=" when several goals are under focus. *)
+Goal exists vl1 : list val,
+  cons (Val LitL) (cons (Val LitL) nil) = vl1 /\
+  (tyref vl1)
+.
+Proof.
+eexists (cons _ (cons _ _)).
+split =>//=.
+Fail progress simpl.
+Abort.
diff --git a/test-suite/ssr/try_case.v b/test-suite/ssr/try_case.v
new file mode 100644
index 0000000000..114bf2cecf
--- /dev/null
+++ b/test-suite/ssr/try_case.v
@@ -0,0 +1,11 @@
+From Coq Require Import ssreflect.
+
+Axiom T : Type.
+Axiom R : T -> T -> Type.
+
+(** Check that internal exceptions are correctly caught in the monad *)
+Goal forall (a b : T) (Hab : R a b), True.
+Proof.
+intros.
+try (case: Hab).
+Abort.