From 664b3cba1e8d326382ca981aa49fdf00edd429e6 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 5 Aug 2014 15:51:16 +0200
Subject: 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.---
 tactics/tacinterp.ml | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1f53e19c36..dea543958a 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))
-- 
cgit v1.2.3