diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ae4cd06022..3e7479903a 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 -> |