diff options
| author | Pierre-Marie Pédrot | 2014-09-18 17:18:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-18 17:23:15 +0200 |
| commit | 892c74d099fd9eda1e2f179645f7e1d9b67ba49b (patch) | |
| tree | fdf2997401cd36359d4e976ac0c4a18bb7f38330 /proofs/proofview.ml | |
| parent | 6d549d3a2b0ab89c77e34646e866584522bd3591 (diff) | |
Fixing strange evarmap leak in goals.
Goals have to be refreshed when observed, because the evarmap may have
changed between the moment where the goal was generated and the moment the
goal is used.
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 75725e47c4..6ecf4da7e6 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -942,8 +942,12 @@ module Goal = struct match Goal.advance sigma goal with | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> - (** The sigma is unchanged. *) - let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in + let gl = + tclEVARMAP >>= fun sigma -> + (** The sigma is unchanged. *) + let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in + tclUNIT gl + in Some gl in tclUNIT (List.map_filter map step.comb) |