From ffda464321e856e44c7f99e6aab201770781c806 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 May 2020 19:04:11 +0200
Subject: Remove call to Refiner API from Funind.

---
 plugins/funind/indfun_common.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/funind/indfun_common.ml')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index e83fe56cc9..0e7d3c2f3b 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_"
@@ -427,6 +427,7 @@ let evaluable_of_global_reference r =
   | _ -> assert false
 
 let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) =
+  let open Tacticals in
   tclREPEAT
     (List.fold_right
        (fun (eq, b) i ->
-- 
cgit v1.2.3


From 1d16c80c53702c3118cc61729a0823d4a9cdaf78 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 May 2020 18:44:32 +0200
Subject: Deprecate the legacy tacticals from module Refiner.

---
 plugins/funind/indfun_common.ml | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

(limited to 'plugins/funind/indfun_common.ml')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 0e7d3c2f3b..af53f16e1f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -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"
@@ -428,15 +429,15 @@ let evaluable_of_global_reference r =
 
 let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) =
   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 ())))
+  (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
-- 
cgit v1.2.3