Merge PR #9153: [api] Move reduction modules to `tactics`

1 files changed, 4 insertions, 3 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 07f50f6cd5..4d817625f5 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -164,11 +164,12 @@ module Btauto = struct
 
   let reify env t = lapp eval [|convert_env env; convert t|]
 
-  let print_counterexample p env gl =
+  let print_counterexample p penv gl =
     let var = lapp witness [|p|] in
     let var = EConstr.of_constr var in
     (* Compute an assignment that dissatisfies the goal *)
-    let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
+    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 var = EConstr.Unsafe.to_constr var in
     let rec to_list l = match decomp_term (Tacmach.project gl) l with
     | App (c, _)
@@ -192,7 +193,7 @@ module Btauto = struct
     let msg =
       try
         let var = to_list var in
-        let assign = List.combine env var in
+        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 = Pfedit.get_current_context () in