diff options
| author | gareuselesinge | 2013-10-31 14:24:46 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-31 14:24:46 +0000 |
| commit | a46165247a22d9f1015dea81a17ee2f5c2ee6099 (patch) | |
| tree | 61fe946caf460e8d888c53914a6b6ab3dabb119c /proofs | |
| parent | 6637d0b8cc876e91ced18cb0ea481463bddfe2eb (diff) | |
Future: better doc + restore ~pure optimization
This optimization was undone because the kernel type checking was
not a pure functions (it was accessing the conv_oracle state imperatively).
Now that the conv_oracle state is part of env, the optimization can be
restored. This was the cause of the increase in memory consumption, since
it was forcing to keep a copy of the system state for every proof, even the
ones that are not delayed/delegated to slaves.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16963 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 7382f438bd..807d833844 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -278,7 +278,7 @@ let close_proof ~now fpl = const_entry_inline_code = false; const_entry_opaque = true }) fpl initial_goals in if now then - List.iter (fun x -> ignore(Future.compute x.Entries.const_entry_body)) entries; + List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries; (pid, (entries, compute_guard, strength, hook)) let return_proof () = @@ -302,7 +302,7 @@ let return_proof () = let close_future_proof proof = close_proof ~now:false proof let close_proof fix_exn = - close_proof ~now:true (Future.from_here ~fix_exn (return_proof ())) + close_proof ~now:true (Future.from_val ~fix_exn (return_proof ())) (**********************************************************) (* *) |