Further port of the SSR tactics.

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