]> matita.cs.unibo.it Git - helm.git/commitdiff
Implementation of existential type improved (more strict checking).
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Jun 2009 21:58:28 +0000 (21:58 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Jun 2009 21:58:28 +0000 (21:58 +0000)
helm/software/components/ng_kernel/nCicLibrary.ml

index 414e5c5de1fad5296fefc5f9fdd8549fbb87ffe6..d28b0da6ce3c423f348c1c423aef745c20c6780e 100644 (file)
@@ -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 =