]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nRstatus.mli
Good:
[helm.git] / helm / software / components / ng_refiner / nRstatus.mli
index 7fde1b74733c5be2348432daf060eb5ce29a0a31..89f62ce1d3c5d42bb79b06a3161af110972ac1b5 100644 (file)
@@ -16,7 +16,10 @@ class status :
   inherit NCicUnifHint.status
   inherit NCicCoercion.status
   inherit NCicLibrary.status
-  method set_rstatus: status -> 'self
+  method set_rstatus: 
+   < coerc_db : NCicCoercion.db;
+     uhint_db : NCicUnifHint.db;
+     timestamp: NCicLibrary.timestamp; .. > -> 'self
  end
 
 module Serializer:
@@ -30,5 +33,9 @@ class dumpable_status :
   inherit status
   method dump: Serializer.obj list
   method set_dump: Serializer.obj list -> 'self
-  method set_dumpable_status: dumpable_status -> 'self
+  method set_dumpable_status:
+   < coerc_db : NCicCoercion.db;
+     uhint_db : NCicUnifHint.db;
+     timestamp: NCicLibrary.timestamp;
+     dump: Serializer.obj list; .. > -> 'self
  end