diff options
| author | Pierre-Marie Pédrot | 2018-12-22 15:25:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-22 15:25:12 +0100 |
| commit | 037c9bc18d34de831997278e31511ddcee6a1426 (patch) | |
| tree | e36c18d28af98972d8d023b038f43e0770adc5f1 /plugins | |
| parent | 6c8d47b07b4f0ec59169ac207b204d2bf2116f3a (diff) | |
| parent | 6ff8870f57797f9bf7c340fb6a4b561e521a1325 (diff) | |
Merge PR #9248: Fix #7904: update proofview env after ltac constr:()
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 -> |