From 7a56397ae26854df6335a3325353d0a5d6c894ea Mon Sep 17 00:00:00 2001 From: amblaf Date: Thu, 15 Jun 2017 11:34:40 +0200 Subject: Remove references to Global.env in tactics/*.ml Only in ml files that are not related to Coq commands --- tactics/eauto.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'tactics/eauto.ml') 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) -- cgit v1.2.3