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 /tactics/ftactic.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 'tactics/ftactic.ml')
| -rw-r--r-- | tactics/ftactic.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml index 43602d1fb6..d8b12fc4e4 100644 --- a/tactics/ftactic.ml +++ b/tactics/ftactic.ml @@ -40,12 +40,13 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function let nf_enter f = bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) (fun gl -> + gl >>= fun gl -> Proofview.Goal.normalize gl >>= fun nfgl -> Proofview.V82.wrap_exceptions (fun () -> f nfgl)) let enter f = bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) - (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) + (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) let lift (type a) (t:a Proofview.tactic) : a t = Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x)) |