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.mli | |
| 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.mli')
| -rw-r--r-- | proofs/proofview.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index bda88178bf..c44707c1e7 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 |