]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nRstatus.mli
...
[helm.git] / helm / software / components / ng_refiner / nRstatus.mli
index 10a4a8a622a5203f7dce1be998b7c373a64f2571..40974aac21c08b68c9d614de44edaae8fa24a349 100644 (file)
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
+class type g_status =
+ object
+  inherit NCicCoercion.g_status
+  inherit NCicLibrary.g_status
+ end
+
 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
+  inherit g_status
+  method set_rstatus: #g_status -> 'self
  end
 
 module Serializer:
@@ -27,14 +31,16 @@ module Serializer:
   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
-  method dump: Serializer.obj list
+  inherit g_dumpable_status
   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
+  method set_dumpable_status: #g_dumpable_status -> 'self
  end