Merge PR #12273: Deprecate Refiner API

Reviewed-by: ejgallego

3 files changed, 46 insertions, 29 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f4200854c2..49fc513dd2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -243,19 +243,25 @@ let change_eq env sigma hyp_id (context : rel_context) x t end_of_type =
   let new_ctxt, new_end_of_type =
     decompose_prod_n_assum sigma ctxt_size new_type_of_hyp
   in
-  let prove_new_hyp : tactic =
-    tclTHEN
-      (tclDO ctxt_size (Proofview.V82.of_tactic intro))
-      (fun g ->
-        let all_ids = pf_ids_of_hyps g in
-        let new_ids, _ = list_chop ctxt_size all_ids in
-        let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in
-        let evm, _ = pf_apply Typing.type_of g to_refine in
-        tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g)
+  let prove_new_hyp =
+    let open Tacticals.New in
+    let open Tacmach.New in
+    tclTHEN (tclDO ctxt_size intro)
+      (Proofview.Goal.enter (fun g ->
+           let all_ids = pf_ids_of_hyps g in
+           let new_ids, _ = list_chop ctxt_size all_ids in
+           let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in
+           let evm, _ =
+             Typing.type_of (Proofview.Goal.env g) (Proofview.Goal.sigma g)
+               to_refine
+           in
+           tclTHEN
+             (Proofview.Unsafe.tclEVARS evm)
+             (Proofview.V82.tactic (refine to_refine))))
   in
   let simpl_eq_tac =
     change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp
-      prove_new_hyp
+      (Proofview.V82.of_tactic prove_new_hyp)
   in
   (*     observe (str "In " ++ Ppconstr.pr_id hyp_id ++  *)
   (*             str "removing an equation " ++ fnl ()++  *)
@@ -534,11 +540,13 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id =
         let prov_hid = pf_get_new_id hid g in
         let c = mkApp (mkVar hid, args) in
         let evm, _ = pf_apply Typing.type_of g c in
-        tclTHENLIST
-          [ Refiner.tclEVARS evm
-          ; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c)
-          ; thin [hid]
-          ; Proofview.V82.of_tactic (rename_hyp [(prov_hid, hid)]) ]
+        let open Tacticals.New in
+        Proofview.V82.of_tactic
+          (tclTHENLIST
+             [ Proofview.Unsafe.tclEVARS evm
+             ; pose_proof (Name prov_hid) c
+             ; clear [hid]
+             ; rename_hyp [(prov_hid, hid)] ])
           g)
       (fun (*
           if not then we are in a mutual function block
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index e83fe56cc9..af53f16e1f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -2,7 +2,7 @@ open Names
 open Pp
 open Constr
 open Libnames
-open Refiner
+open Tacmach
 
 let mk_prefix pre id = Id.of_string (pre ^ Id.to_string id)
 let mk_rel_id = mk_prefix "R_"
@@ -395,7 +395,8 @@ let jmeq_refl () =
   with e when CErrors.noncritical e -> raise (ToShow e)
 
 let h_intros l =
-  tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l
+  Proofview.V82.of_tactic
+    (Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l)
 
 let h_id = Id.of_string "h"
 let hrec_id = Id.of_string "hrec"
@@ -427,15 +428,16 @@ let evaluable_of_global_reference r =
   | _ -> assert false
 
 let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) =
-  tclREPEAT
-    (List.fold_right
-       (fun (eq, b) i ->
-         tclORELSE
-           (Proofview.V82.of_tactic
-              ((if b then Equality.rewriteLR else Equality.rewriteRL) eq))
-           i)
-       (if rev then List.rev eqs else eqs)
-       (tclFAIL 0 (mt ())))
+  let open Tacticals in
+  (tclREPEAT
+     (List.fold_right
+        (fun (eq, b) i ->
+          tclORELSE
+            (Proofview.V82.of_tactic
+               ((if b then Equality.rewriteLR else Equality.rewriteRL) eq))
+            i)
+        (if rev then List.rev eqs else eqs)
+        (tclFAIL 0 (mt ()))) [@ocaml.warning "-3"])
 
 let decompose_lam_n sigma n =
   if n < 0 then
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5c82ed38bb..9b2d9c4815 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -703,9 +703,16 @@ let terminate_letin (na, b, t, e) expr_info continuation_tac info g =
   in
   continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g
 
-let pf_type c tac gl =
-  let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
-  tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
+let pf_type c tac =
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      let evars, ty = Typing.type_of env sigma c in
+      tclTHEN (Proofview.Unsafe.tclEVARS evars) (tac ty))
+
+let pf_type c tac =
+  Proofview.V82.of_tactic (pf_type c (fun ty -> Proofview.V82.tactic (tac ty)))
 
 let pf_typel l tac =
   let rec aux tys l =