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