Further port of the SSR tactics.

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. ********************************************************)