From a46165247a22d9f1015dea81a17ee2f5c2ee6099 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 31 Oct 2013 14:24:46 +0000 Subject: 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 --- kernel/cooking.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/cooking.ml') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index dbe83a856..0a1d713c4 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -126,7 +126,7 @@ let on_body f = function | Undef _ as x -> x | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs))) | OpaqueDef lc -> - OpaqueDef (Future.chain lc (fun lc -> + OpaqueDef (Future.chain ~pure:true lc (fun lc -> (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc))))) let constr_of_def = function -- cgit v1.2.3