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

When "entering" in a goal, the environment observed by [tclENV] is changed (in the scope of the goal) to be that of the goal.

I'm not entirely sure it is the right semantics. But it allows to write tactics which are agnostic of whether they are run in a goal or not.

4 files changed, 30 insertions, 3 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index d207a0382..74f41d071 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -549,6 +549,8 @@ let tclEVARMAP =
 
 let tclENV = Proof.current
 
+let tclIN_ENV = Proof.set_local
+
 let tclEFFECTS eff =
   Proof.modify (fun initial -> emit_side_effects eff initial)
 
@@ -875,6 +877,9 @@ module Goal = struct
   end
 
   let 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 ->
@@ -892,6 +897,9 @@ 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 165f7a9b5..bc414a791 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -246,11 +246,16 @@ val tclPROGRESS : 'a tactic -> 'a tactic
 val tclEVARMAP : Evd.evar_map tactic
 
 (* [tclENV] doesn't affect the proof, it returns the current
-   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}. *)
+   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. *)
 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 d3e2b8df7..285cb9574 100644
--- a/proofs/proofview_monad.ml
+++ b/proofs/proofview_monad.ml
@@ -247,6 +247,18 @@ 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 ab92a57fc..07d61375e 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -131,6 +131,8 @@ 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