From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 16 Jun 2009 21:58:28 +0000 (+0000)
Subject: Implementation of existential type improved (more strict checking).
X-Git-Tag: make_still_working~3861
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=33435f271509f4888d44f9446b078eeebbe71519;p=helm.git

Implementation of existential type improved (more strict checking).
---

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 414e5c5de..d28b0da6c 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -72,7 +72,7 @@ module type Serializer =
 module Serializer(S: sig type status end) =
  struct
   type status = S.status
-  type obj = Obj.t
+  type obj = string * Obj.t
 
   let require1 = ref (fun _ -> assert false (* unknown data*))
   let already_registered = ref []
@@ -82,14 +82,14 @@ module Serializer(S: sig type status end) =
    already_registered := tag :: !already_registered;
    require1 :=
     (fun (tag',data) as x ->
-     if tag=tag' then Obj.magic require data else Obj.magic !require1 x);
-   Obj.magic (fun x -> tag,x)
+     if tag=tag' then require (Obj.magic data) else !require1 x);
+   (fun x -> tag,Obj.repr x)
 
   let serialize = serialize
 
   let require ~baseuri status =
    let dump = require0 ~baseuri in
-    List.fold_right (Obj.magic !require1) dump status
+    List.fold_right !require1 dump status
 end
 
 let decompile ~baseuri =