X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnRstatus.mli;h=40974aac21c08b68c9d614de44edaae8fa24a349;hb=d43b4cfa41256e90fceb0129b7eadb38207190c3;hp=6cf9ddd4fa9c136b77ff8c4cc14b771e55a06880;hpb=5c8de084e314e41f3dc2f605f6242283e930b803;p=helm.git

diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli
index 6cf9ddd4f..40974aac2 100644
--- a/helm/software/components/ng_refiner/nRstatus.mli
+++ b/helm/software/components/ng_refiner/nRstatus.mli
@@ -11,9 +11,36 @@
 
 (* $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;
-        dump: refiner_status -> refiner_status
-}
+class type g_status =
+ object
+  inherit NCicCoercion.g_status
+  inherit NCicLibrary.g_status
+ end
+
+class status :
+ object ('self)
+  inherit NCicCoercion.status
+  inherit NCicLibrary.status
+  inherit g_status
+  method set_rstatus: #g_status -> 'self
+ end
+
+module Serializer:
+ sig
+  include NCicLibrary.Serializer with type status = status 
+  val require: baseuri:NUri.uri -> (#status as 'status) -> 'status
+ end
+
+class type g_dumpable_status =
+ object
+  inherit g_status
+  method dump: Serializer.obj list
+ end
+
+class dumpable_status :
+ object ('self)
+  inherit status
+  inherit g_dumpable_status
+  method set_dump: Serializer.obj list -> 'self
+  method set_dumpable_status: #g_dumpable_status -> 'self
+ end