From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 27 Jul 2009 12:24:52 +0000 (+0000)
Subject: Serious bug fixed: because of lazy evaluation of !require1, the function could
X-Git-Tag: make_still_working~3612
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a04fc65f5bbe94395cdf4397c6f9682457f4e9cd;p=helm.git

Serious bug fixed: because of lazy evaluation of !require1, the function could
diverge.
---

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