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

This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6.

Conflicts:
	proofs/proofview.ml

1 files changed, 0 insertions, 7 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 32df96097f..2c104ea181 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 ->