From 6ff8870f57797f9bf7c340fb6a4b561e521a1325 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 19 Dec 2018 10:51:04 +0100
Subject: Fix #7904: update proofview env after ltac constr:()

(in case of side effects)

Also:
Fix #4781
Fix #4496
---
 plugins/ltac/tacinterp.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 816741b894..5a9c8ff641 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1957,7 +1957,9 @@ let lifts f = (); fun ist x -> Ftactic.enter begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let (sigma, v) = f ist env sigma x in
   Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-  (Ftactic.return v)
+    (* FIXME once we don't need to catch side effects *)
+    (Proofview.tclTHEN (Proofview.Unsafe.tclSETENV (Global.env()))
+       (Ftactic.return v))
 end
 
 let interp_bindings' ist bl = Ftactic.return begin fun env sigma ->
-- 
cgit v1.2.3