diff options
| author | Gaëtan Gilbert | 2018-12-19 10:51:04 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-19 17:27:44 +0100 |
| commit | 6ff8870f57797f9bf7c340fb6a4b561e521a1325 (patch) | |
| tree | 45379ca41065ad0a2780666dbdcfc1eada836e64 /plugins | |
| parent | 2cad4dec40cef2aecb19c5a0e5a1368392be8d88 (diff) | |
Fix #7904: update proofview env after ltac constr:()
(in case of side effects)
Also:
Fix #4781
Fix #4496
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 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 -> |