Moving the remaining Refiner functions to Tacmach.

1 files changed, 2 insertions, 2 deletions

diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index c78cc96a83..43f70dfecc 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -335,7 +335,7 @@ let unwrap g_s =
   match g_s with
   | Some g_s ->
     let goal = Evd.sig_it g_s in
-    let sigma = Refiner.project g_s in
+    let sigma = Tacmach.project g_s in
     goal_info goal sigma
   | None -> ([], CString.Map.empty, Pp.mt ())
 
@@ -545,7 +545,7 @@ let match_goals ot nt =
 
 let get_proof_context (p : Proof.t) =
   let Proof.{goals; sigma} = Proof.data p in
-  sigma, Refiner.pf_env { Evd.it = List.(hd goals); sigma }
+  sigma, Tacmach.pf_env { Evd.it = List.(hd goals); sigma }
 
 let to_constr pf =
   let open CAst in