From 913ccc7fb4a987ddd7c591d3c7d75579dc502a95 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Dec 2018 08:07:32 +0100
Subject: [api] Move reduction modules to `tactics`

These modules do actually belong there.

We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
---
 plugins/btauto/refl_btauto.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/btauto')

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
-- 
cgit v1.2.3