From 04a8c766a51b17997d8a9ffcf6f2d7beffc599ce Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 15:35:40 +0200
Subject: Remove a critical call to V82.tactic in Clenvtac.

Despite being marked as a breaking change by myself, it seems that the
underlying condition had been solved in the meantime.
---
 proofs/clenvtac.ml | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 767f93787d..197d69a481 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'))
+    (Proofview.V82.tactic (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))))
   end
 
 let clenv_pose_dependent_evars ?(with_evars=false) clenv =
-- 
cgit v1.2.3


From 1109581ba7afca804515fc6179565da808bae4f7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 15:57:54 +0200
Subject: Wrap Refiner.refiner in the tactic monad.

This function was used almost everywhere with the wrapper around.
---
 plugins/funind/functional_principles_proofs.ml | 5 ++++-
 plugins/ssr/ssrcommon.ml                       | 2 +-
 plugins/ssr/ssrelim.ml                         | 2 +-
 proofs/clenvtac.ml                             | 2 +-
 proofs/refiner.ml                              | 2 ++
 proofs/refiner.mli                             | 2 +-
 tactics/equality.ml                            | 8 ++++----
 tactics/tactics.ml                             | 4 ++--
 8 files changed, 16 insertions(+), 11 deletions(-)

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/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 134a9e4b36..95a0790ff3 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1014,7 +1014,7 @@ 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
 
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index b44600a8cf..8f445b4397 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -477,7 +477,7 @@ let revtoptac n0 gl =
   let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) 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
+  Proofview.V82.of_tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])))) gl
 
 let equality_inj l b id c gl =
   let msg = ref "" in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 197d69a481..695e103082 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -77,7 +77,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
   let clenv = { clenv with evd = evd' } in
   Proofview.tclTHEN
     (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd'))
-    (Proofview.V82.tactic (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))))
+    (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..6a0ba30bbf 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 (refiner ~check c)
+
 (*********************)
 (*   Tacticals       *)
 (*********************)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 66eae1db81..d4f2239a59 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. } *)
 
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/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)))
-- 
cgit v1.2.3


From 6839a2c9b7d2480e21572a7d176dcd6ea0617159 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 16:05:19 +0200
Subject: Remove a very specific low-level tactical from Refiner.

It was only used at one point in the STM, and its localization was suprising
to say the least. Furthermore it was relying on legacy code. Instead we hardcode
it in the STM.
---
 proofs/refiner.ml  | 2 --
 proofs/refiner.mli | 1 -
 stm/stm.ml         | 6 +++++-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 6a0ba30bbf..ad84afd47e 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -271,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 d4f2239a59..3471f38e9e 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -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 ()
-- 
cgit v1.2.3


From a704c05e4722e9fa994d98a961eee87faa28bc4c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 16:10:31 +0200
Subject: Remove a call to V82.tactic in Btauto.

---
 plugins/btauto/refl_btauto.ml | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

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
-- 
cgit v1.2.3


From c459cbd09ec16dd7e6767ac4ffe55e19747f4705 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 2 May 2020 01:20:35 +0200
Subject: Wrap a monadic combinator in a try-with block to catch exceptions.

Moving code around uncovered this bug.
---
 plugins/ssr/ssrcommon.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 95a0790ff3..a0d90dcf0d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1321,7 +1321,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
-- 
cgit v1.2.3


From 86751a2069fd3360742d44dbe66c221894196ad6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 16:13:35 +0200
Subject: Wrap ssr tactics into V82.tactic.

Porting them is still to be done, but at least we don't rely on the wrapper
everywhere.
---
 plugins/ssr/ssrbwd.ml                 |  2 +-
 plugins/ssr/ssrcommon.ml              | 18 +++++---
 plugins/ssr/ssrcommon.mli             | 10 ++---
 plugins/ssr/ssrelim.ml                | 20 ++++++---
 plugins/ssr/ssrelim.mli               |  4 +-
 plugins/ssr/ssrequality.ml            | 24 +++++++----
 plugins/ssr/ssrequality.mli           |  8 ++--
 plugins/ssr/ssrfwd.ml                 | 30 ++++++++-----
 plugins/ssr/ssrfwd.mli                | 10 ++---
 plugins/ssr/ssripats.ml               | 16 +++----
 plugins/ssr/ssrparser.mlg             | 81 ++++++++++++++++-------------------
 plugins/ssr/ssrtacticals.ml           | 16 ++++---
 plugins/ssr/ssrtacticals.mli          |  6 +--
 plugins/ssrmatching/g_ssrmatching.mlg |  2 +-
 plugins/ssrmatching/ssrmatching.ml    |  4 +-
 plugins/ssrmatching/ssrmatching.mli   |  2 +-
 16 files changed, 139 insertions(+), 114 deletions(-)

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


From fcef4f7d643d40cb652580e507d7bda914e8b9f2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 17:35:21 +0200
Subject: Further port SSReflect tactics to the new engine.

---
 plugins/ssr/ssrcommon.ml    | 28 ++++++++++++++++------------
 plugins/ssr/ssrcommon.mli   |  2 +-
 plugins/ssr/ssrequality.ml  | 10 +++++++---
 plugins/ssr/ssrequality.mli |  4 ++--
 plugins/ssr/ssripats.ml     |  6 +++---
 5 files changed, 29 insertions(+), 21 deletions(-)

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 7e7cd8b4a1..bcdcd0af4a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1173,7 +1173,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));
@@ -1181,11 +1182,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) =
-  Proofview.V82.tactic ~nf_evars:false begin fun gl ->
-  tclTHENLIST (old_cleartac clr :: List.rev_map gentac gens)
-  gl end
+  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
@@ -1195,7 +1195,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)
 ;;
@@ -1222,20 +1222,24 @@ let pfLIFT f =
  * 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 =
-  Proofview.V82.tactic ~nf_evars:false begin fun gl ->
-  let c, gl = pf_mkSsrConst "protect_term" gl in
-  let prot, _ = EConstr.destConst (project gl) c in
-  Tacticals.onClause (fun idopt ->
+  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, c = mkSsrConst "protect_term" env sigma in
+  let prot, _ = EConstr.destConst sigma c in
+  Proofview.Unsafe.tclEVARS sigma <*>
+  Tacticals.New.onClause (fun idopt ->
     let hyploc = Option.map (fun id -> id, InHyp) idopt in
-    Proofview.V82.of_tactic (Tactics.reduct_option ~check:false
+    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
+           CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc)
+    allHypsAndConcl
   end
 
 let is_protect hd env sigma =
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 9229b6d384..f655457c63 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -355,7 +355,7 @@ val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> 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) *
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 1a73bfded0..33a2eb85d9 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -66,6 +66,8 @@ let simpltac = function
   | SimplCut (n,m) -> tclTHEN (safe_simpltac m) (tclTRY (Proofview.V82.of_tactic (donetac n)))
   | Nop -> tclIDTAC
 
+let simpltac s = Proofview.V82.tactic ~nf_evars:false (simpltac s)
+
 (** The "congr" tactic *)
 
 let interp_congrarg_at ist gl n rf ty m =
@@ -197,7 +199,7 @@ let simplintac occ rdx sim gl =
         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
+      Proofview.V82.of_tactic (simpltac (Simpl m)) gl
     end else
       let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
       let simp env c _ _ = EConstr.Unsafe.to_constr (red_safe Tacred.simpl env sigma0 (EConstr.of_constr c)) in
@@ -207,7 +209,7 @@ let simplintac occ rdx sim gl =
   match sim with
   | Simpl m -> simptac m gl
   | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (Proofview.V82.of_tactic (donetac n))) gl
-  | _ -> simpltac sim gl
+  | _ -> Proofview.V82.of_tactic (simpltac sim) gl
 
 let rec get_evalref env sigma c = match EConstr.kind sigma c with
   | Var id -> EvalVarRef id
@@ -627,7 +629,9 @@ let ssrinstancesofrule ist dir arg =
   with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); tclIDTAC gl
   end
 
-let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl
+let ipat_rewrite occ dir c = Proofview.V82.tactic ~nf_evars:false begin fun gl ->
+  rwrxtac occ None dir (project gl, c) gl
+end
 
 let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
   let fail = ref false in
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index fc2b75b396..1c3b1bb018 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -26,7 +26,7 @@ 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 ->
@@ -61,7 +61,7 @@ val ssrrewritetac :
   Ltac_plugin.Tacinterp.interp_sign ->
    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 ->
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 7fba7ff830..16fd5235a2 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 *)
@@ -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
 
-- 
cgit v1.2.3


From 87e811844fa980200cd23eea2b51fd525152e134 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 2 May 2020 14:09:03 +0200
Subject: Export missing tacticals.

---
 tactics/tacticals.ml  | 3 +++
 tactics/tacticals.mli | 1 +
 2 files changed, 4 insertions(+)

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
 
-- 
cgit v1.2.3


From 40892bcd8f578154f49fe6086e123b1766b3e3e3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 18:01:39 +0200
Subject: Slightly more tricky port of the ssr tactics.

---
 plugins/ssr/ssrtacticals.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 37e4b625f0..6d3c5d8807 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
@@ -45,20 +47,18 @@ let rot_hyps dir i hyps =
   rot (match dir with L2R -> i | R2L -> n - i) [] hyps
 
 let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) =
-  Proofview.V82.tactic begin
   let i = get_index ivar in
-  let evtac t = Proofview.V82.of_tactic (ssrevaltac ist t) in
+  let 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))
-  end
+  | 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 *)(* {{{ **********************************************)
 
-- 
cgit v1.2.3


From cc3e6f34038ab546d74ed535f47a3909caf8fa53 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 18:09:40 +0200
Subject: Further porting of ssrcode.

---
 plugins/ssr/ssrbwd.ml       |  4 ++--
 plugins/ssr/ssrcommon.ml    | 12 ++++++------
 plugins/ssr/ssrcommon.mli   |  6 ++++--
 plugins/ssr/ssrequality.ml  | 25 +++++++++++++------------
 plugins/ssr/ssrtacticals.ml | 10 +++++-----
 5 files changed, 30 insertions(+), 27 deletions(-)

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 692b13c2bb..53a5190c99 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -55,7 +55,7 @@ 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
@@ -63,7 +63,7 @@ let interp_nbargs ist gl rc =
 
 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
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index bcdcd0af4a..6cbb92163e 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -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
@@ -845,7 +845,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
@@ -917,7 +917,7 @@ 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 (pf_env gl) (project gl) ist ty) in
    let ty =
      let env = pf_env gl in
      if not resolve_typeclasses then ty
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index f655457c63..a8b95c39ff 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 :
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 33a2eb85d9..7fe673873f 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -89,7 +89,7 @@ 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 =
@@ -484,8 +484,7 @@ let closed0_check cl p gl =
 
 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 =
@@ -564,7 +563,7 @@ let rwprocess_rule dir rule gl =
 
 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 r_sigma, rules = rwprocess_rule env dir rule in
   let find_rule rdx =
     let rec rwtac = function
       | [] ->
@@ -604,10 +603,12 @@ let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl =
 ;;
 
 let ssrinstancesofrule ist dir arg =
-  Proofview.V82.tactic begin fun gl ->
-  let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
-  let rule = interp_term ist gl arg in
-  let r_sigma, rules = rwprocess_rule dir rule gl in
+  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) =
@@ -624,9 +625,9 @@ let ssrinstancesofrule ist dir arg =
   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 sigma0 concl0) 1 ~k:print)
     done; raise NoMatch
-  with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); tclIDTAC gl
+  with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); Tacticals.New.tclIDTAC
   end
 
 let ipat_rewrite occ dir c = Proofview.V82.tactic ~nf_evars:false begin fun gl ->
@@ -639,7 +640,7 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt)
     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
+    try interp_term (pf_env gl) (project gl) ist 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
@@ -679,7 +680,7 @@ let unfoldtac occ ko t kt gl =
 let unlocktac ist args =
   Proofview.V82.tactic begin fun gl ->
   let utac (occ, gt) gl =
-    unfoldtac occ occ (interp_term ist gl gt) (fst gt) gl in
+    unfoldtac occ occ (interp_term (pf_env gl) (project gl) ist gt) (fst gt) gl in
   let locked, gl = pf_mkSsrConst "locked" gl in
   let key, gl = pf_mkSsrConst "master_key" gl in
   let ktacs = [
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 6d3c5d8807..4f9747ae73 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -151,15 +151,15 @@ let tclCLAUSES tac (gens, clseq) =
 (** The "do" tactical. ********************************************************)
 
 let hinttac ist is_by (is_or, atacs) =
-  Proofview.V82.tactic begin
-  let dtac = if is_by then Proofview.V82.of_tactic (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) =
-- 
cgit v1.2.3


From cd74849bc46a4ba933cfd86e1aff55ec6ccf4125 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 18:34:35 +0200
Subject: Export new combinators in SSR not relying on the legacy API.

---
 plugins/ssr/ssrcommon.ml  | 34 ++++++++++++++++++++++------------
 plugins/ssr/ssrcommon.mli | 18 ++++++++++++++++++
 2 files changed, 40 insertions(+), 12 deletions(-)

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 6cbb92163e..d643132588 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -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
 
 
@@ -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 =
@@ -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 =
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index a8b95c39ff..d6ab326b10 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -181,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 ->
@@ -241,6 +256,9 @@ 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
-- 
cgit v1.2.3


From c1b1afe76e1655cc3275bdf4215f0ab690efc3cc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 19:00:19 +0200
Subject: Further port of the SSR code.

---
 plugins/ssr/ssrbwd.ml      |  6 +++---
 plugins/ssr/ssrcommon.ml   | 19 +++++++++++++------
 plugins/ssr/ssrcommon.mli  |  4 ++--
 plugins/ssr/ssrelim.ml     |  2 +-
 plugins/ssr/ssrequality.ml |  6 +++---
 plugins/ssr/ssrfwd.ml      |  2 +-
 6 files changed, 23 insertions(+), 16 deletions(-)

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 53a5190c99..0674d3d28a 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -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,7 +112,7 @@ 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))
@@ -148,7 +148,7 @@ 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
 )
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d643132588..6ab0a16789 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -993,7 +993,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
@@ -1029,13 +1030,19 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t g
          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   *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index d6ab326b10..5db55eca91 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -335,7 +335,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 ->
@@ -359,7 +359,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 ->
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 8c9dcd9972..b3fa1ea9d0 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -453,7 +453,7 @@ 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]
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 7fe673873f..c2ee180855 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -107,7 +107,7 @@ 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
@@ -373,8 +373,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
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index dcf9c1f7db..708833c52f 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -128,7 +128,7 @@ let havetac ist
      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
+     Proofview.V82.of_tactic (applyn ~with_evars:true ~with_shelve:false 2 step) gl
    else basecuttac "ssr_have" t gl in
  (* Introduce now abstract constants, so that everything sees them *)
  let abstract_key, gl = pf_mkSsrConst "abstract_key" gl in
-- 
cgit v1.2.3


From db6fc85ed67e2db7be5d5b8b2dbdbfb37655a5ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 23:37:15 +0200
Subject: Further port of the SSR tactics.

---
 plugins/ssr/ssrbwd.ml       | 12 ++++----
 plugins/ssr/ssrcommon.ml    | 23 +++++++--------
 plugins/ssr/ssrcommon.mli   |  4 +--
 plugins/ssr/ssrelim.ml      |  4 +--
 plugins/ssr/ssrequality.ml  | 12 ++++----
 plugins/ssr/ssrfwd.ml       | 68 ++++++++++++++++++++++++++-------------------
 plugins/ssr/ssrfwd.mli      |  2 +-
 plugins/ssr/ssrtacticals.ml |  4 +--
 8 files changed, 72 insertions(+), 57 deletions(-)

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 0674d3d28a..32a215444b 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -119,11 +119,13 @@ let refine_interp_apply_view dbl ist gl gv =
         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
@@ -150,7 +152,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:
     let gl = pf_merge_uc_of sigma gl in
     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 6ab0a16789..29f52d8834 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1060,23 +1060,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
@@ -1314,8 +1315,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)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 5db55eca91..362e488d8a 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -398,7 +398,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 :
@@ -427,7 +427,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 b3fa1ea9d0..6155f8fbf6 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -519,8 +519,8 @@ let perform_injection c =
   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) (Proofview.V82.tactic (injectidl2rtac id id_with_ebind)) in
+  Proofview.V82.of_tactic (Tacticals.New.tclTHENLAST (Tactics.apply (EConstr.compose_lam dc cl1)) injtac) gl
   end
 
 let ssrscase_or_inj_tac c =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index c2ee180855..1e3e2e69ea 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -420,12 +420,12 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
       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, gl
       | _ ->
           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
+          Proofview.V82.of_tactic (convert_concl ~check:true cl'), Proofview.V82.tactic (rewritetac ?under dir r'), gl
     else
       let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
       let r3, _, r3t  =
@@ -435,9 +435,9 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
       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 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
+      let cltac = Tactics.clear [pattern_id; rule_id] in
+      let rwtacs = [Proofview.V82.tactic (rewritetac ?under dir (EConstr.mkVar rule_id)); cltac] in
+      apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), gl
   in
   let cvtac' _ =
     try cvtac gl with
@@ -452,7 +452,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
           (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl)
         ++ error)
   in
-  tclTHEN cvtac' rwtac gl
+  tclTHEN cvtac' (Proofview.V82.of_tactic rwtac) gl
 
 [@@@ocaml.warning "-3"]
 let lz_coq_prod =
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 708833c52f..8173db000a 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -59,7 +59,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) =
   | 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
@@ -89,11 +89,17 @@ 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 basecuttac name 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, hd = mkSsrConst name env sigma 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 sigma, _ = Typing.type_of env sigma t in
+  Proofview.Unsafe.tclEVARS sigma <*>
+  Tactics.apply t
+  end
 
 let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats)
 
@@ -123,13 +129,19 @@ let havetac ist
    not !ssrhaveNOtcresolution &&
    match fk with FwdHint(_,true) -> false | _ -> true in
  let hint = Proofview.V82.of_tactic (hinttac ist true hint) in
- let cuttac t gl =
+ let cuttac t =
+  let open Proofview.Notations in
+  Proofview.Goal.enter begin fun gl ->
    if transp then
-     let have_let, gl = pf_mkSsrConst "ssr_have_let" gl in
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+     let sigma, have_let = mkSsrConst "ssr_have_let" env sigma in
      let step = EConstr.mkApp (have_let, [|concl;t|]) in
-     let gl, _ = pf_e_type_of gl step in
-     Proofview.V82.of_tactic (applyn ~with_evars:true ~with_shelve:false 2 step) gl
-   else basecuttac "ssr_have" t gl in
+     let sigma, _ = Typing.type_of env sigma step in
+     Proofview.Unsafe.tclEVARS sigma <*>
+     applyn ~with_evars:true ~with_shelve:false 2 step
+   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 =
@@ -203,7 +215,7 @@ let havetac ist
      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
    | _, true, false -> assert false in
-  Tacticals.tclTHENS (cuttac cut) [ Tacticals.tclTHEN sol itac1; itac2 ] gl)
+  Tacticals.tclTHENS (Proofview.V82.of_tactic (cuttac cut)) [ Tacticals.tclTHEN sol itac1; itac2 ] gl)
  gl
 end
 
@@ -264,41 +276,41 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave =
          | LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args)
          | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in
     c, args, pired c args, pf_merge_uc uc gl in
-  let tacipat pats = introstac pats in
+  let tacipat pats = Proofview.V82.tactic (introstac pats) in
   let tacigens =
-    Tacticals.tclTHEN
-      (Tacticals.tclTHENLIST(List.rev(List.fold_right mkclr gens [old_cleartac clr0])))
-      (introstac (List.fold_right mkpats gens [])) in
-  let hinttac = Proofview.V82.of_tactic (hinttac ist true hint) in
+    Tacticals.New.tclTHEN
+      (Tacticals.New.tclTHENLIST(List.rev(List.fold_right mkclr gens [cleartac clr0])))
+      (Proofview.V82.tactic (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 *)
@@ -324,7 +336,7 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
   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
+    Proofview.V82.of_tactic (basecuttac "ssr_suff" ty) gl in
   Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))]
   end
 
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 2de10837c5..dc90b159d7 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -31,7 +31,7 @@ val havetac : ist ->
 
 val basecuttac :
            string ->
-           EConstr.t -> Goal.goal Evd.sigma -> Evar.t list Evd.sigma
+           EConstr.t -> unit Proofview.tactic
 
 val wlogtac :
   Ltac_plugin.Tacinterp.interp_sign ->
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 4f9747ae73..a379b2561a 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -132,7 +132,7 @@ let tclCLAUSES tac (gens, clseq) =
   Proofview.V82.tactic begin fun gl ->
   if clseq = InGoal || clseq = InSeqGoal then tac gl else
   let clr_gens = pf_clauseids gl gens clseq in
-  let clear = Tacticals.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in
+  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.pf_ids_of_hyps gl) in
   let cl0 = pf_concl gl in
   let dtac gl =
@@ -145,7 +145,7 @@ let tclCLAUSES tac (gens, clseq) =
       | _, 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.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; Proofview.V82.of_tactic clear; tac; endtac]) gl
   end
 
 (** The "do" tactical. ********************************************************)
-- 
cgit v1.2.3


From a9f3d9b8e6f70f08fdda24947caf9a4d2317c4ea Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 00:13:17 +0200
Subject: Further port of SSR tactics.

---
 plugins/ssr/ssrfwd.ml | 42 +++++++++++++++++++++---------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 8173db000a..b2e6f69e95 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -101,7 +101,7 @@ let basecuttac name c =
   Tactics.apply t
   end
 
-let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats)
+let introstac ipats = tclIPAT ipats
 
 let havetac ist
   (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint)))
@@ -119,16 +119,16 @@ 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 = Proofview.V82.of_tactic (hinttac ist true hint) in
+ let hint = hinttac ist true hint in
  let cuttac t =
   let open Proofview.Notations in
   Proofview.Goal.enter begin fun gl ->
@@ -147,7 +147,7 @@ let havetac ist
  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
@@ -180,7 +180,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
@@ -198,13 +198,13 @@ 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 ->
+     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 ->
             let abstract, gl = pf_mkSsrConst "abstract" gl in
-            Proofview.V82.of_tactic (unfold [abstract; abstract_key]) 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
@@ -213,9 +213,9 @@ 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 (Proofview.V82.of_tactic (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
 
@@ -276,11 +276,11 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave =
          | LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args)
          | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in
     c, args, pired c args, pf_merge_uc uc gl in
-  let tacipat pats = Proofview.V82.tactic (introstac pats) in
+  let tacipat pats = introstac pats in
   let tacigens =
     Tacticals.New.tclTHEN
       (Tacticals.New.tclTHENLIST(List.rev(List.fold_right mkclr gens [cleartac clr0])))
-      (Proofview.V82.tactic (introstac (List.fold_right mkpats gens []))) in
+      (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
@@ -316,12 +316,11 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave =
 (** The "suffice" tactic *)
 
 let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
-  Proofview.V82.tactic begin
   let clr = Option.default [] clr in
   let pats = tclCompileIPats pats in
   let binders = tclCompileIPats binders in
   let simpl = tclCompileIPats simpl in
-  let htac = Tacticals.tclTHEN (introstac pats) (Proofview.V82.of_tactic (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
@@ -334,11 +333,12 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
     | _ -> anomaly "suff: ssr cast hole deleted by typecheck"
     end
   in
-  let ctac gl =
+  let ctac =
+    Proofview.V82.tactic begin fun gl ->
     let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
-    Proofview.V82.of_tactic (basecuttac "ssr_suff" ty) gl in
-  Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))]
-  end
+    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
 
-- 
cgit v1.2.3


From f13c800114b8cf378fe7d52757d310923a46737e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 00:48:28 +0200
Subject: Remove legacy layer in SSR.

---
 plugins/ssr/ssrcommon.ml            |  8 ++--
 plugins/ssr/ssrelim.ml              |  6 +--
 plugins/ssr/ssrequality.ml          |  2 +-
 plugins/ssr/ssrfwd.ml               |  2 +-
 plugins/ssr/ssripats.ml             |  4 +-
 plugins/ssrmatching/ssrmatching.ml  | 79 +++++++++++++++----------------------
 plugins/ssrmatching/ssrmatching.mli |  4 +-
 7 files changed, 45 insertions(+), 60 deletions(-)

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 29f52d8834..e0a1cbce3a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1144,7 +1144,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 =
@@ -1287,7 +1287,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
@@ -1300,7 +1300,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
@@ -1489,7 +1489,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 =
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 6155f8fbf6..60ffe6ceb6 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 *)
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 1e3e2e69ea..1e4faa3eee 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -637,7 +637,7 @@ end
 let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
   let fail = ref false in
   let interp_rpattern gl gc =
-    try interp_rpattern gl gc
+    try interp_rpattern (pf_env gl) (project gl) gc
     with _ when snd mult = May -> fail := true; project gl, T mkProp in
   let interp gc gl =
     try interp_term (pf_env gl) (project gl) ist gc
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index b2e6f69e95..6ff59f21a3 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -43,7 +43,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) =
   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
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 16fd5235a2..c102111e52 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -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 =
@@ -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/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 6a36959e83..cc2345c7f8 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
@@ -173,8 +172,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 +929,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 +963,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 +971,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 +989,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 +1000,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 +1052,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 +1066,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 +1080,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)
@@ -1286,18 +1266,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 +1290,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 =
@@ -1321,7 +1306,7 @@ let ssrinstancesof arg =
 (*   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 sigma0, cpat = interp_cpattern (pf_env gl) (project gl) 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 =
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 176dfa92b2..4a30544a74 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
 
-- 
cgit v1.2.3


From 20ee46f95d2198ea32750a7991ec9571c9eb2bb1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 12:00:02 +0200
Subject: Further SSR port.

---
 plugins/ssr/ssrequality.ml         |  2 +-
 plugins/ssrmatching/ssrmatching.ml | 17 +++++++++--------
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 1e4faa3eee..d52b83d529 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -625,7 +625,7 @@ let ssrinstancesofrule ist dir arg =
   Feedback.msg_info Pp.(str"BEGIN INSTANCES");
   try
     while true do
-      ignore(find env0 (EConstr.to_constr sigma0 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"); Tacticals.New.tclIDTAC
   end
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index cc2345c7f8..30957bbc79 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -21,7 +21,6 @@ open CoqConstr
 open Vars
 open Libnames
 open Tactics
-open Tacticals
 open Termops
 open Recordops
 open Tacmach
@@ -1301,25 +1300,27 @@ let () =
   Mltop.declare_cache_obj obj "ssrmatching_plugin"
 
 let ssrinstancesof arg =
-  Proofview.V82.tactic begin fun gl ->
+  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 (pf_env gl) (project 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 =
-- 
cgit v1.2.3


From d6b6d77c4998355bd4db0517f964c9db1937439c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 13:23:25 +0200
Subject: Remove legacy SSR API.

---
 plugins/ssr/ssrbwd.ml               |  6 +++---
 plugins/ssr/ssrcommon.ml            | 10 +++++-----
 plugins/ssr/ssrcommon.mli           |  6 +++---
 plugins/ssr/ssrequality.ml          |  2 +-
 plugins/ssrmatching/ssrmatching.ml  |  8 ++++----
 plugins/ssrmatching/ssrmatching.mli |  2 ++
 6 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 32a215444b..42b9248979 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -58,7 +58,7 @@ let interp_nbargs ist gl rc =
     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 =
@@ -66,7 +66,7 @@ let interp_view_nbimps ist gl rc =
     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
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e0a1cbce3a..64c4914054 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 =
@@ -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
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 362e488d8a..00b2e56221 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -155,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
@@ -262,8 +262,8 @@ val abs_evars_pirrel :
 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 ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index d52b83d529..6036642fbd 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -95,7 +95,7 @@ let congrtac ((n, t), ty) ist gl =
   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
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 30957bbc79..adaf7c8cc1 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -1224,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 =
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 4a30544a74..17b47227cb 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -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
 
-- 
cgit v1.2.3


From 4ee015b32fbb41850d06cda24a2c8375b1034c7c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 13:40:29 +0200
Subject: Further SSR port.

---
 plugins/ssr/ssrequality.ml | 67 +++++++++++++++++++++++++++++-----------------
 1 file changed, 43 insertions(+), 24 deletions(-)

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 6036642fbd..45426362fb 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -42,31 +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
-    Proofview.V82.of_tactic (ssr_n_tac "simpl" n) gl
+    ssr_n_tac "simpl" n
 
 let simpltac = function
   | Simpl n -> safe_simpltac n
-  | Cut n -> tclTRY (Proofview.V82.of_tactic (donetac n))
-  | SimplCut (n,m) -> tclTHEN (safe_simpltac m) (tclTRY (Proofview.V82.of_tactic (donetac n)))
-  | Nop -> tclIDTAC
+  | 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.V82.tactic ~nf_evars:false (simpltac s)
+let simpltac s = Proofview.Goal.enter (fun _ -> simpltac s)
 
 (** The "congr" tactic *)
 
@@ -669,22 +674,36 @@ let ssrrewritetac ?under ?map_redex ist rwargs =
 
 (** 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
+  convert_concl ~check:true (Reductionops.clos_norm_flags f env sigma cl')
+  end
 
 let unlocktac ist args =
-  Proofview.V82.tactic begin fun gl ->
-  let utac (occ, gt) gl =
-    unfoldtac occ occ (interp_term (pf_env gl) (project gl) ist gt) (fst gt) gl in
-  let locked, gl = pf_mkSsrConst "locked" gl in
-  let key, gl = pf_mkSsrConst "master_key" gl in
+  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 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
+  let sigma, locked = mkSsrConst "locked" env sigma in
+  let sigma, key = mkSsrConst "master_key" env sigma in
   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
+  Proofview.Unsafe.tclEVARS sigma <*>
+  Tacticals.New.tclTHENLIST (List.map utac args @ ktacs)
   end
-- 
cgit v1.2.3


From 2f45e79b02126ebb80daf9d47cc0333971f3380b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 15:19:09 +0200
Subject: Further port of the SSR tactics.

---
 plugins/ssr/ssrcommon.ml    | 19 ++++++++++++-------
 plugins/ssr/ssrcommon.mli   |  2 +-
 plugins/ssr/ssrequality.ml  | 29 ++++++++++++++++++-----------
 plugins/ssr/ssrtacticals.ml |  2 +-
 4 files changed, 32 insertions(+), 20 deletions(-)

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 64c4914054..238b94ae49 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1105,16 +1105,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
@@ -1125,11 +1126,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
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 00b2e56221..b82478a23a 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -410,7 +410,7 @@ 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 : unit Proofview.tactic
 val is_protect : EConstr.t -> Environ.env -> Evd.evar_map -> bool
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 45426362fb..668395aa37 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -639,27 +639,34 @@ let ipat_rewrite occ dir c = Proofview.V82.tactic ~nf_evars:false begin fun gl -
   rwrxtac occ None dir (project gl, c) gl
 end
 
-let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
+let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) =
+  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 (pf_env gl) (project gl) gc
     with _ when snd mult = May -> fail := true; project gl, T mkProp in
-  let interp gc gl =
-    try interp_term (pf_env gl) (project gl) ist gc
-    with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in
-  let rwtac gl =
+  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.V82.tactic begin fun 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 t = interp (pf_env gl) (project gl) gt in
     let gl = pf_merge_uc_of (fst t) gl in
     (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) gl
+    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 *)
 
@@ -668,8 +675,8 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt)
 (** The "rewrite" tactic *)
 
 let ssrrewritetac ?under ?map_redex ist rwargs =
-  Proofview.V82.tactic begin fun gl ->
-  tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs) gl
+  Proofview.Goal.enter begin fun _ ->
+  Tacticals.New.tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs)
   end
 
 (** The "unlock" tactic *)
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index a379b2561a..26fd463124 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -164,4 +164,4 @@ let hinttac ist is_by (is_or, atacs) =
 
 let ssrdotac ist (((n, m), tac), clauses) =
   let mul = get_index n, m in
-  tclCLAUSES (Proofview.V82.tactic (tclMULT mul (Proofview.V82.of_tactic (hinttac ist false tac)))) clauses
+  tclCLAUSES (tclMULT mul (hinttac ist false tac)) clauses
-- 
cgit v1.2.3


From 89b34bfce82fb5f328f75618c252eccb3242a9d0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 15:57:59 +0200
Subject: Further port of the SSR tactics.

---
 plugins/ssr/ssrelim.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 60ffe6ceb6..f49abe8fec 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -392,10 +392,12 @@ 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 =
+            Proofview.V82.tactic ~nf_evars:false begin fun s ->
             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 }
+            end
           in
           gen_eq_tac, eq_ty, gl in
         let rel = k + if c_is_head_p then 1 else 0 in
@@ -403,7 +405,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 =
@@ -455,7 +457,6 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
     Tacticals.New.tclTHENLIST [
       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]
 ;;
 
-- 
cgit v1.2.3


From 107917615048f29c3a7d55d3648a734061cc23fc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 16:01:54 +0200
Subject: Further port of the SSR tactics.

---
 plugins/ssr/ssrelim.ml | 31 +++++++++++++++++++------------
 1 file changed, 19 insertions(+), 12 deletions(-)

diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index f49abe8fec..cab71c2e73 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -492,15 +492,17 @@ let equality_inj l b id c gl =
     Feedback.msg_warning (Pp.str !msg);
     discharge_hyp (id, (id, "")) gl
 
-let injectidl2rtac id c gl =
+let injectidl2rtac id c =
+  Proofview.V82.tactic begin fun gl ->
   Tacticals.tclTHEN (equality_inj None true id c) (revtoptac (pf_nb_prod gl)) gl
+  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 env sigma c =
   let sigma, cty = Typing.type_of env sigma c in
@@ -508,20 +510,25 @@ let is_injection_case env sigma c =
   Coqlib.check_ind_ref "core.eq.type" mind
 
 let perform_injection c =
-  Proofview.V82.tactic ~nf_evars:false begin fun gl ->
-  let gl, cty = pfe_type_of gl c in
-  let mind, t = pf_reduce_to_quantified_ind gl cty in
-  let dc, eqt = EConstr.decompose_prod (project gl) t in
-  if dc = [] then injectl2rtac (project gl) c gl else
-  if not (EConstr.Vars.closed0 (project gl) eqt) then
+  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.New.tclTHEN (introid id) (Proofview.V82.tactic (injectidl2rtac id id_with_ebind)) in
-  Proofview.V82.of_tactic (Tacticals.New.tclTHENLAST (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 =
-- 
cgit v1.2.3


From 1d1465eea0908512811d312cf8b07c38d3b02941 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 16:08:25 +0200
Subject: Further port of the SSR tactics.

---
 plugins/ssr/ssrelim.ml | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index cab71c2e73..551c316e79 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -473,14 +473,19 @@ 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
-  Proofview.V82.of_tactic (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
@@ -491,10 +496,13 @@ 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 =
-  Proofview.V82.tactic begin fun gl ->
-  Tacticals.tclTHEN (equality_inj None true id c) (revtoptac (pf_nb_prod gl)) gl
+  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
-- 
cgit v1.2.3


From 2183239d03c506ec38134f689b7509285ddff0a2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 16:28:02 +0200
Subject: Further port of the SSR tactics.

---
 plugins/ssr/ssrelim.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 551c316e79..4148102f61 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -393,10 +393,13 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
           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 =
-            Proofview.V82.tactic ~nf_evars:false begin fun s ->
+            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
-- 
cgit v1.2.3


From 2d00c8b07957206040dbc71598439a601eef4161 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 16:32:02 +0200
Subject: Further port of the SSR tactics

---
 plugins/ssr/ssrelim.ml      |  2 --
 plugins/ssr/ssrtacticals.ml | 30 +++++++++++++++++-------------
 2 files changed, 17 insertions(+), 15 deletions(-)

diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 4148102f61..8e75ba7a2b 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -471,8 +471,6 @@ 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"
 
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 26fd463124..cbc352126e 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -76,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
@@ -84,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
@@ -126,26 +127,29 @@ 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")
+  end
 
 let tclCLAUSES tac (gens, clseq) =
-  let tac = Proofview.V82.of_tactic tac in
-  Proofview.V82.tactic begin fun gl ->
-  if clseq = InGoal || clseq = InSeqGoal then tac gl else
-  let clr_gens = pf_clauseids gl gens clseq in
+  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.pf_ids_of_hyps gl) in
-  let cl0 = pf_concl gl in
-  let dtac gl =
+  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; Proofview.V82.of_tactic clear; tac; endtac]) gl
+  Tacticals.New.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; clear; tac; endtac])
   end
 
 (** The "do" tactical. ********************************************************)
-- 
cgit v1.2.3


From ea11e308be5f7410ea0f032736eb6ec2e686abbe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 16:38:21 +0200
Subject: Remove legacy API in SSR.

---
 plugins/ssr/ssrcommon.ml  | 9 ++++-----
 plugins/ssr/ssrcommon.mli | 3 ++-
 plugins/ssr/ssrfwd.ml     | 6 +++---
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 238b94ae49..1cc879559d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -902,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) ->
@@ -927,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 (pf_env gl) (project gl) ist 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
 ;;
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index b82478a23a..e1d6061178 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -320,8 +320,9 @@ 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
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 6ff59f21a3..d319eba8aa 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -152,7 +152,7 @@ let havetac ist
   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)}) ->
@@ -261,7 +261,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave =
     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
@@ -335,7 +335,7 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
   in
   let ctac =
     Proofview.V82.tactic begin fun gl ->
-    let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
+    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))]
-- 
cgit v1.2.3


From bb2a078e3ed2bb13b14838ae7d35883450cb14c7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 16:44:09 +0200
Subject: Further port of the SSR tactics.

---
 plugins/ssr/ssrequality.ml | 37 +++++++++++++++++++++----------------
 1 file changed, 21 insertions(+), 16 deletions(-)

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 668395aa37..993ff78926 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -404,7 +404,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
       (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty))
 ;;
 
-let rwcltac ?under ?map_redex cl rdx dir sr gl =
+let rwcltac ?under ?map_redex cl rdx dir sr =
+  Proofview.V82.tactic begin fun gl ->
   let sr =
     let sigma, r = sr in
     let sigma = resolve_typeclasses ~where:r ~fail:false (pf_env gl) sigma in
@@ -458,6 +459,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
         ++ error)
   in
   tclTHEN cvtac' (Proofview.V82.of_tactic rwtac) gl
+  end
 
 [@@@ocaml.warning "-3"]
 let lz_coq_prod =
@@ -483,9 +485,9 @@ 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
 
@@ -566,15 +568,17 @@ let rwprocess_rule env dir rule =
   in
     r_sigma, rules
 
-let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl =
-  let env = pf_env 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
@@ -582,7 +586,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
@@ -594,18 +599,18 @@ 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
-;;
+  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 ->
@@ -635,8 +640,8 @@ let ssrinstancesofrule ist dir arg =
   with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); Tacticals.New.tclIDTAC
   end
 
-let ipat_rewrite occ dir c = Proofview.V82.tactic ~nf_evars:false begin fun gl ->
-  rwrxtac occ None dir (project gl, c) gl
+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))) =
@@ -661,7 +666,7 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt)
     (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
+    | RWeq -> Proofview.V82.of_tactic (rwrxtac ?under ?map_redex occ rx dir t)) gl
     end
   in
   let ctac = cleartac (interp_clr sigma (oclr, (fst gt, snd (interp env sigma gt)))) in
-- 
cgit v1.2.3


From 2fb11a6d18235854bc0a3d82fcec9c09afb58a50 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 16:51:58 +0200
Subject: Further port of the SSR tactics.

---
 plugins/ssr/ssrequality.ml | 43 +++++++++++++++++++++++++++----------------
 1 file changed, 27 insertions(+), 16 deletions(-)

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 993ff78926..b67d59857e 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -197,7 +197,8 @@ 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 simplintac occ rdx sim =
+  Proofview.V82.tactic begin fun gl ->
   let simptac m gl =
     if m <> ~-1 then begin
       if rdx <> None then
@@ -215,6 +216,7 @@ let simplintac occ rdx sim gl =
   | Simpl m -> simptac m gl
   | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (Proofview.V82.of_tactic (donetac n))) gl
   | _ -> Proofview.V82.of_tactic (simpltac sim) gl
+  end
 
 let rec get_evalref env sigma c = match EConstr.kind sigma c with
   | Var id -> EvalVarRef id
@@ -242,7 +244,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
@@ -295,9 +298,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
@@ -322,7 +326,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
 
@@ -644,29 +648,36 @@ let ipat_rewrite occ dir c = Proofview.Goal.enter begin fun gl ->
   rwrxtac occ None dir (Proofview.Goal.sigma gl, c)
 end
 
+let pf_merge_uc_of s sigma =
+  Evd.merge_universe_context sigma (Evd.evar_universe_context s)
+
 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 (pf_env gl) (project gl) gc
-    with _ when snd mult = May -> fail := true; project gl, T mkProp 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.V82.tactic begin fun 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 (pf_env gl) (project gl) gt in
-    let gl = pf_merge_uc_of (fst t) gl in
+    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 -> Proofview.V82.of_tactic (rwrxtac ?under ?map_redex occ rx dir t)) 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
-- 
cgit v1.2.3


From 64d593021c6cd689c62ce36c5842062a4f4516d4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 17:12:01 +0200
Subject: Further port of SSR tactics.

---
 plugins/ssr/ssrcommon.ml   |  2 +-
 plugins/ssr/ssrcommon.mli  |  2 +-
 plugins/ssr/ssrequality.ml | 71 +++++++++++++++++++++++++---------------------
 3 files changed, 41 insertions(+), 34 deletions(-)

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1cc879559d..d2e521fb50 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -845,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
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index e1d6061178..e1c3b051d7 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -371,7 +371,7 @@ 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
 
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index b67d59857e..92aad98ffb 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -350,7 +350,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
@@ -406,63 +407,72 @@ 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 =
-  Proofview.V82.tactic begin fun gl ->
+  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, Tacticals.New.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'), Proofview.V82.tactic (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 = Tactics.clear [pattern_id; rule_id] in
-      let rwtacs = [Proofview.V82.tactic (rewritetac ?under dir (EConstr.mkVar rule_id)); cltac] in
-      apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), gl
+      let rwtacs = [rewritetac ?under dir (EConstr.mkVar rule_id); cltac] in
+      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' (Proofview.V82.of_tactic rwtac) gl
+  Proofview.Unsafe.tclEVARS sigma0 <*>
+  Tacticals.New.tclTHEN cvtac' rwtac
   end
 
 [@@@ocaml.warning "-3"]
@@ -648,9 +658,6 @@ let ipat_rewrite occ dir c = Proofview.Goal.enter begin fun gl ->
   rwrxtac occ None dir (Proofview.Goal.sigma gl, c)
 end
 
-let pf_merge_uc_of s sigma =
-  Evd.merge_universe_context sigma (Evd.evar_universe_context s)
-
 let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) =
   let open Proofview.Notations in
   Proofview.Goal.enter begin fun gl ->
-- 
cgit v1.2.3


From 81024e4f9dfef4d8240cc26be97b8b10cfa8bf1f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 17:27:44 +0200
Subject: Further port of ssr tactics

---
 plugins/ssr/ssrequality.ml | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 92aad98ffb..6bfd500b3c 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -198,24 +198,26 @@ let norwmult = L2R, nomult
 let norwocc = noclr, None
 
 let simplintac occ rdx sim =
-  Proofview.V82.tactic begin fun gl ->
-  let simptac m gl =
+  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");
-      Proofview.V82.of_tactic (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 (Proofview.V82.of_tactic (donetac n))) gl
-  | _ -> Proofview.V82.of_tactic (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
-- 
cgit v1.2.3


From 596963894ce798d7515fea4a317c074c718c16df Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 May 2020 20:08:20 +0200
Subject: Add overlays.

---
 dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh

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
-- 
cgit v1.2.3


From 4add482cfde2e3734be567c9824b2774871deb52 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 2 May 2020 18:58:39 +0200
Subject: Add tests uncovered during bug chasing in the CI.

---
 test-suite/ssr/simpl_done.v | 28 ++++++++++++++++++++++++++++
 test-suite/ssr/try_case.v   | 11 +++++++++++
 2 files changed, 39 insertions(+)
 create mode 100644 test-suite/ssr/simpl_done.v
 create mode 100644 test-suite/ssr/try_case.v

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.
-- 
cgit v1.2.3


From 6678c067abac278554ab205ab18315d30202a369 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 4 May 2020 15:14:53 +0200
Subject: [ssr] get rid of (pf_)mkSsrConst

---
 plugins/ssr/ssrcommon.ml   | 53 +++++++++++++++++++++++-----------------------
 plugins/ssr/ssrcommon.mli  |  9 +-------
 plugins/ssr/ssrequality.ml | 13 +++++-------
 plugins/ssr/ssrfwd.ml      | 44 ++++++++++++++++----------------------
 plugins/ssr/ssrfwd.mli     |  4 +---
 plugins/ssr/ssripats.ml    |  8 +++----
 6 files changed, 55 insertions(+), 76 deletions(-)

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d2e521fb50..06b26b28fd 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1240,30 +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 =
-  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, c = mkSsrConst "protect_term" env sigma in
-  let prot, _ = EConstr.destConst sigma c in
-  Proofview.Unsafe.tclEVARS sigma <*>
-  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
-  end
-
 let is_protect hd env sigma =
   let _, protectC = mkSsrConst "protect_term" env sigma in
   EConstr.eq_constr_nounivs sigma hd protectC
@@ -1521,12 +1497,35 @@ 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 tacMK_SSR_CONST name =
+  Proofview.tclENV >>= fun env ->
+  Proofview.tclEVARMAP >>= fun sigma ->
   let sigma, c = mkSsrConst name env sigma in
   Unsafe.tclEVARS sigma <*>
   tclUNIT c
-end
+
+let tacDEST_CONST c =
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let c, _ = EConstr.destConst sigma c in
+  tclUNIT c
+
+(* 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 e1c3b051d7..d1ad24496e 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -233,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 ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 6bfd500b3c..ab07dd5be9 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -120,6 +120,9 @@ let pf_typecheck t gl =
   re_sig [it] sigma
 
 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)));
@@ -137,7 +140,6 @@ let newssrcongrtac arg ist =
     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 *)
@@ -720,9 +722,6 @@ let unfoldtac occ ko t kt =
 
 let unlocktac ist args =
   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 utac (occ, gt) =
     Proofview.Goal.enter begin fun gl ->
       let env = Proofview.Goal.env gl in
@@ -730,12 +729,10 @@ let unlocktac ist args =
       unfoldtac occ occ (interp_term env sigma ist gt) (fst gt)
     end
   in
-  let sigma, locked = mkSsrConst "locked" env sigma in
-  let sigma, key = mkSsrConst "master_key" env sigma in
+  Ssrcommon.tacMK_SSR_CONST "locked" >>= fun locked ->
+  Ssrcommon.tacMK_SSR_CONST "master_key" >>= fun key ->
   let ktacs = [
     (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) xInParens);
     Ssrelim.casetac key (fun ?seed:_ k -> k)
   ] in
-  Proofview.Unsafe.tclEVARS sigma <*>
   Tacticals.New.tclTHENLIST (List.map utac args @ ktacs)
-  end
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index d319eba8aa..4961138190 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -89,17 +89,19 @@ 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 =
+let basecuttac name t =
   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, hd = mkSsrConst name env sigma in
-  let t = EConstr.mkApp (hd, [|c|]) in
-  let sigma, _ = Typing.type_of env sigma t in
-  Proofview.Unsafe.tclEVARS sigma <*>
+  Ssrcommon.tacMK_SSR_CONST name >>= fun hd ->
+  let t = EConstr.mkApp (hd, [|t|]) in
+  Ssrcommon.tacTYPEOF t >>= fun _ty ->
   Tactics.apply t
-  end
+
+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
 
@@ -107,6 +109,9 @@ let havetac ist
   (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint)))
   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
@@ -129,21 +134,11 @@ let havetac ist
    not !ssrhaveNOtcresolution &&
    match fk with FwdHint(_,true) -> false | _ -> true in
  let hint = hinttac ist true hint in
- let cuttac t =
-  let open Proofview.Notations in
-  Proofview.Goal.enter begin fun gl ->
-   if transp then
-    let env = Proofview.Goal.env gl in
-    let sigma = Proofview.Goal.sigma gl in
-     let sigma, have_let = mkSsrConst "ssr_have_let" env sigma in
-     let step = EConstr.mkApp (have_let, [|concl;t|]) in
-     let sigma, _ = Typing.type_of env sigma step in
-     Proofview.Unsafe.tclEVARS sigma <*>
-     applyn ~with_evars:true ~with_shelve:false 2 step
+ 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
@@ -203,7 +198,6 @@ let havetac ist
      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 ->
-            let abstract, gl = pf_mkSsrConst "abstract" gl in
             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
@@ -361,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
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index dc90b159d7..33bf56cfa9 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -29,9 +29,7 @@ val havetac : ist ->
            bool ->
            bool -> unit Proofview.tactic
 
-val basecuttac :
-           string ->
-           EConstr.t -> unit Proofview.tactic
+val basecuttac : string -> EConstr.t -> unit Proofview.tactic
 
 val wlogtac :
   Ltac_plugin.Tacinterp.interp_sign ->
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index c102111e52..46f90a7ee1 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -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
 
-- 
cgit v1.2.3


From 64ce136a5fb2eb1d3b620889b2047fda82694849 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 5 May 2020 10:21:21 +0200
Subject: [ssr] wrap a couple of exception with tclLIFT

---
 plugins/ssr/ssrcommon.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 06b26b28fd..e05c4c26dd 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1500,14 +1500,17 @@ end
 let tacMK_SSR_CONST name =
   Proofview.tclENV >>= fun env ->
   Proofview.tclEVARMAP >>= fun sigma ->
-  let sigma, c = mkSsrConst name env sigma in
-  Unsafe.tclEVARS sigma <*>
-  tclUNIT c
+  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 ->
-  let c, _ = EConstr.destConst sigma c in
-  tclUNIT c
+  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
-- 
cgit v1.2.3


From d87f8d10d089c3a33ddb36a71ab6fc082d0d1140 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 May 2020 09:00:49 +0200
Subject: Fix GeoCoq slowdown.

There is no point in normalizing the goal in the legacy refiner because the
function is actually insensitive to evars.
---
 proofs/refiner.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ad84afd47e..29a47c5acd 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -37,7 +37,7 @@ let refiner ~check =
       CProfile.profile2 refiner_key (refiner ~check)
   else refiner ~check
 
-let refiner ~check c = Proofview.V82.tactic (refiner ~check c)
+let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c)
 
 (*********************)
 (*   Tacticals       *)
-- 
cgit v1.2.3