]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicLibrary.mli
FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:
[helm.git] / helm / software / components / ng_kernel / nCicLibrary.mli
index 11a608e1da89af9471780685a8e04ba6833bbe43..f94c656827dc48d6fe0c205c15a4305c7406b319 100644 (file)
@@ -25,8 +25,17 @@ val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *)
 val clear_cache : unit -> unit
 
 val time_travel: timestamp -> unit
-val serialize: baseuri:NUri.uri -> ('status -> 'status) -> unit
-val require: baseuri:NUri.uri -> 'status -> 'status
 val decompile: baseuri:NUri.uri -> unit
 
+module type Serializer =
+ sig
+  type status
+  type obj
+  val register: string -> ('a -> status -> status) -> ('a -> obj)
+  val serialize: baseuri:NUri.uri -> obj list -> unit
+  val require: baseuri:NUri.uri -> status -> status
+ end
+
+module Serializer(S: sig type status end): Serializer with type status= S.status
+
 (* EOF *)