]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nRstatus.mli
Code simplified.
[helm.git] / helm / software / components / ng_refiner / nRstatus.mli
index 89f62ce1d3c5d42bb79b06a3161af110972ac1b5..631e629e5a663060a1f314fdd738ff809cc90ad9 100644 (file)
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
-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
+class type g_status = NCicCoercion.status
 
-module Serializer:
- sig
-  include NCicLibrary.Serializer with type status = status 
-  val require: baseuri:NUri.uri -> (#status as 'status) -> 'status
- end
+class status : NCicCoercion.status
 
-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