]> matita.cs.unibo.it Git - helm.git/commitdiff
Serious bug fixed: because of lazy evaluation of !require1, the function could
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Jul 2009 12:24:52 +0000 (12:24 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Jul 2009 12:24:52 +0000 (12:24 +0000)
diverge.

helm/software/components/ng_kernel/nCicLibrary.ml

index 6d1797677a6f23b8c587afe71709990f9e4189b1..33276cc3df689942cd19391af7e2c30d92647d1c 100644 (file)
@@ -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