Remove references to Global.env in tactics/*.ml

Only in ml files that are not related to Coq commands

1 files changed, 3 insertions, 3 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 64d4d3135..3d073c9dc 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -86,16 +86,16 @@ let rec prolog l n gl =
   let prol = (prolog l (n-1)) in
   (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
 
-let out_term = function
+let out_term env = function
   | IsConstr (c, _) -> c
-  | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance (Global.env ()) gr))
+  | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr))
 
 let prolog_tac l n =
   Proofview.V82.tactic begin fun gl ->
   let map c =
     let (sigma, c) = c (pf_env gl) (project gl) in
     let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in
-    out_term c
+    out_term (pf_env gl) c
   in
   let l = List.map map l in
   try (prolog l n gl)