X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnRstatus.mli;h=89f62ce1d3c5d42bb79b06a3161af110972ac1b5;hb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;hp=729f6ba6eec5e65f93ac85837d388193c9ac9368;hpb=f6c887944d48d718f372a57f1609f3d059908aa8;p=helm.git

diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli
index 729f6ba6e..89f62ce1d 100644
--- a/helm/software/components/ng_refiner/nRstatus.mli
+++ b/helm/software/components/ng_refiner/nRstatus.mli
@@ -11,15 +11,31 @@
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
-type refiner_status = {
-        coerc_db : NCicCoercion.db;
-        uhint_db : NCicUnifHint.db;
-        library_db : NCicLibrary.timestamp;
-}
+class status :
+ object ('self)
+  inherit NCicUnifHint.status
+  inherit NCicCoercion.status
+  inherit NCicLibrary.status
+  method set_rstatus: 
+   < coerc_db : NCicCoercion.db;
+     uhint_db : NCicUnifHint.db;
+     timestamp: NCicLibrary.timestamp; .. > -> 'self
+ end
 
-module Serializer: NCicLibrary.Serializer with type status = refiner_status
+module Serializer:
+ sig
+  include NCicLibrary.Serializer with type status = status 
+  val require: baseuri:NUri.uri -> (#status as 'status) -> 'status
+ end
 
-type dumpable_refiner_status = {
-        refiner_status : refiner_status;
-        dump: Serializer.obj list
-}
+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