]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nRstatus.mli
snapshot for CSC
[helm.git] / helm / software / components / ng_refiner / nRstatus.mli
index 46634a6799785e7e81b8df74b8cdc7722ccaccd4..10a4a8a622a5203f7dce1be998b7c373a64f2571 100644 (file)
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
-type refiner_status = {
-        coerc_db : NCicCoercion.db;
-        uhint_db : NCicUnifHint.db;
-}
+class status :
+ object ('self)
+  inherit NCicCoercion.status
+  inherit NCicLibrary.status
+  method set_rstatus: 
+   < coerc_db : NCicCoercion.db;
+     uhint_db : NCicUnifHint.db;
+     timestamp: NCicLibrary.timestamp; .. > -> 'self
+ end
+
+module Serializer:
+ sig
+  include NCicLibrary.Serializer with type status = status 
+  val require: baseuri:NUri.uri -> (#status as 'status) -> 'status
+ end
+
+class dumpable_status :
+ object ('self)
+  inherit status
+  method dump: Serializer.obj list
+  method set_dump: Serializer.obj list -> 'self
+  method set_dumpable_status:
+   < coerc_db : NCicCoercion.db;
+     uhint_db : NCicUnifHint.db;
+     timestamp: NCicLibrary.timestamp;
+     dump: Serializer.obj list; .. > -> 'self
+ end