diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-17 18:53:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-17 19:10:55 +0100 |
| commit | 8a179389fe5199e79d05b2c72ff2aae2061820aa (patch) | |
| tree | 5ffaca3f0ab4faaf8b21f8ca05b6e20def9f9c91 /proofs | |
| parent | 65b901534649c5f29e245a4960fa66f6e9d9c257 (diff) | |
Fixing the Proofview.Goal.goal function.
The environment put in the goals was not the right one and could lead to
various leaks.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 49228c93a..6d7dcb925 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1000,7 +1000,6 @@ module Goal = struct end let goals = - Env.get >>= fun env -> Pv.get >>= fun step -> let sigma = step.solution in let map goal = @@ -1008,6 +1007,7 @@ module Goal = struct | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> let gl = + Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> tclUNIT (gmake env sigma goal) in |