Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."

This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6.

Conflicts:
	proofs/proofview.ml

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))