diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-18 17:18:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-18 17:23:15 +0200 |
| commit | 892c74d099fd9eda1e2f179645f7e1d9b67ba49b (patch) | |
| tree | fdf2997401cd36359d4e976ac0c4a18bb7f38330 | |
| 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.
| -rw-r--r-- | proofs/proofview.ml | 8 | ||||
| -rw-r--r-- | proofs/proofview.mli | 2 | ||||
| -rw-r--r-- | tactics/ftactic.ml | 3 |
3 files changed, 9 insertions, 4 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 75725e47c..6ecf4da7e 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) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index bda88178b..c44707c1e 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -416,7 +416,7 @@ module Goal : sig val enter : ([ `LZ ] t -> unit tactic) -> unit tactic (** Recover the list of current goals under focus, without evar-normalization *) - val goals : [ `LZ ] t list tactic + val goals : [ `LZ ] t tactic list tactic (* compatibility: avoid if possible *) val goal : [ `NF ] t -> Goal.goal diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml index 43602d1fb..d8b12fc4e 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)) |