]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nRstatus.ml
Slightly simplied status code.
[helm.git] / helm / software / components / ng_refiner / nRstatus.ml
index dc7a6cf4a6df00fbad5997308c58e4ac04cd43c1..68fdf4f50f07663efdee6d131280f50f323f2416 100644 (file)
@@ -21,8 +21,7 @@ class status =
  object (self)
   inherit NCicCoercion.status
   inherit NCicLibrary.status
-  method set_rstatus
-   : 'status. #g_status as 'status -> 'self
+  method set_rstatus : 'status. #g_status as 'status -> 'self
    = fun o -> (self#set_coercion_status o)#set_library_status o
  end
 
@@ -47,12 +46,11 @@ class type g_dumpable_status =
  end
 
 class dumpable_status =
- object
+ object(self)
   inherit status
   val dump = ([] : Serializer.obj list)
   method dump = dump
   method set_dump v = {< dump = v >}
-  method set_dumpable_status
-   : 'status. #g_dumpable_status as 'status -> 'self
-   = fun o -> {< dump = o#dump >}#set_rstatus o
+  method set_dumpable_status : 'status. #g_dumpable_status as 'status -> 'self
+   = fun o -> (self#set_dump o#dump)#set_rstatus o
  end