From fc7a66d58c39e3d57e509c754fb4cefa96ecd488 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 4 Sep 2014 12:12:03 +0200 Subject: Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]." This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6. Conflicts: proofs/proofview.ml --- proofs/proofview.ml | 7 ------- proofs/proofview.mli | 11 +++-------- proofs/proofview_monad.ml | 12 ------------ proofs/proofview_monad.mli | 2 -- tactics/tacinterp.ml | 16 ++-------------- 5 files changed, 5 insertions(+), 43 deletions(-) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 32df96097..2c104ea18 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -547,8 +547,6 @@ let tclEVARMAP = let tclENV = Proof.current -let tclIN_ENV = Proof.set_local - let tclEFFECTS eff = Proof.modify (fun initial -> emit_side_effects eff initial) @@ -854,8 +852,6 @@ module Goal = struct end let enter f = - (* the global environment of the tactic is changed to that of - the goal *) list_iter_goal () begin fun goal () -> Proof.current >>= fun env -> tclEVARMAP >>= fun sigma -> @@ -872,9 +868,6 @@ module Goal = struct end let raw_enter f = - (* the global environment of the tactic is changed to that of - the goal *) - let f gl = Proof.set_local (env gl) (f gl) in list_iter_goal () begin fun goal () -> Proof.current >>= fun env -> tclEVARMAP >>= fun sigma -> diff --git a/proofs/proofview.mli b/proofs/proofview.mli index b1466fcfb..f59ad0dc1 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -243,16 +243,11 @@ val tclPROGRESS : 'a tactic -> 'a tactic val tclEVARMAP : Evd.evar_map tactic (* [tclENV] doesn't affect the proof, it returns the current - environment. It can be the global context or, in the context of a - {!Proofview.Goal.enter}, the context of the goal. In the latter - case, the context is the same as the environment returned by - {!Proofview.Goal.env} on the enclosing goal. *) + environment. It is not the environment of a particular goal, + rather the "global" environment of the proof. The goal-wise + environment is returned by {!Proofview.Goal.env}. *) val tclENV : Environ.env tactic -(* [tclIN_ENV e t] is the same as tactic [t] except that the global - environment it observes (obtained by {!tclENV}) is [e]. *) -val tclIN_ENV : Environ.env -> 'a tactic -> 'a tactic - (* [tclEFFECTS eff] add the effects [eff] to the current state. *) val tclEFFECTS : Declareops.side_effects -> unit tactic diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml index a322f8f5b..3781324a6 100644 --- a/proofs/proofview_monad.ml +++ b/proofs/proofview_monad.ml @@ -253,18 +253,6 @@ struct let current : rt tactic = (); fun s -> { iolist = fun nil cons -> cons (s.rstate, s) nil } - let set_local (type a) (rstate : rt) (t:a tactic) : a tactic = (); fun s -> - let tl = t { s with rstate } in - let reinstate = s.rstate in - { iolist = fun nil cons -> - tl.iolist nil (fun (a,s') nil -> cons (a, { s' with rstate=reinstate }) nil)} - - let modify_local (type a) (f:rt->rt) (t:a tactic) : a tactic = (); fun s -> - let tl = t { s with rstate = f s.rstate } in - let reinstate = s.rstate in - { iolist = fun nil cons -> - tl.iolist nil (fun (a,s') nil -> cons (a, { s' with rstate=reinstate }) nil)} - let put (w : wt) : unit tactic = (); fun s -> { iolist = fun nil cons -> cons ((), { s with wstate = merge w s.wstate }) nil } diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index c2a1ff52c..a459db424 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -134,8 +134,6 @@ module Logical : sig val modify : (logicalState -> logicalState) -> unit t val put : logicalMessageType -> unit t val current : logicalEnvironment t - val set_local : logicalEnvironment -> 'a t -> 'a t - val modify_local : (logicalEnvironment->logicalEnvironment) -> 'a t -> 'a t val zero : exn -> 'a t val plus : 'a t -> (exn -> 'a t) -> 'a t diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f241b6373..b35955e24 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1034,23 +1034,11 @@ struct let enter f = bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) - (fun gl -> - (* the global environment of the tactic is changed to that of - the goal *) - Proofview.tclIN_ENV (Proofview.Goal.env gl) ( - Proofview.V82.wrap_exceptions (fun () -> f gl) - ) - ) + (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) let raw_enter f = bind (Proofview.Goal.raw_goals >>= fun l -> Proofview.tclUNIT (Depends l)) - (fun gl -> - (* the global environment of the tactic is changed to that of - the goal *) - Proofview.tclIN_ENV (Proofview.Goal.env gl) ( - Proofview.V82.wrap_exceptions (fun () -> f gl) - ) - ) + (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) let lift (type a) (t:a Proofview.tactic) : a t = Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x)) -- cgit v1.2.3