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.

1 files changed, 14 insertions, 2 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1f53e19c3..dea543958 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -978,11 +978,23 @@ struct
 
   let enter f =
     bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l))
-      (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
+      (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)
+        )
+      )
 
   let raw_enter f =
     bind (Proofview.Goal.raw_goals >>= fun l -> Proofview.tclUNIT (Depends l))
-      (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
+      (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)
+        )
+      )
 
   let lift (type a) (t:a Proofview.tactic) : a t =
     Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x))