From a04fc65f5bbe94395cdf4397c6f9682457f4e9cd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Jul 2009 12:24:52 +0000 Subject: [PATCH] Serious bug fixed: because of lazy evaluation of !require1, the function could diverge. --- helm/software/components/ng_kernel/nCicLibrary.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 6d1797677..33276cc3d 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -200,12 +200,13 @@ module Serializer(S: sig type status end) = let register tag require = assert (not (List.mem tag !already_registered)); already_registered := tag :: !already_registered; + let old_require1 = !require1 in require1 := - (fun (tag',data) as x -> - if tag=tag' then - require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term - else - !require1 x); + (fun (tag',data) as x -> + if tag=tag' then + require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term + else + old_require1 x); (fun x -> tag,Obj.repr x) let serialize = serialize -- 2.39.2