Objects are now used to represent also the tactic status.

[helm.git] / helm / software / components / ng_refiner / nRstatus.ml

diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml
index 736de4aa061cc18acdca68ed0c3a0f013c6b825c..5ef83ec3c2c10ec578e3b0c5c603a94469d50278 100644 (file)
--- a/helm/software/components/ng_refiner/nRstatus.ml
+++ b/helm/software/components/ng_refiner/nRstatus.ml
@@ -11,11 +11,23 @@
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
-class status =
- object
+class type ctstatus =
+ object ('self)
   inherit NCicUnifHint.status
   inherit NCicCoercion.status
   inherit NCicLibrary.status
+  method set_rstatus : ctstatus -> 'self
+ end
+
+class status : ctstatus =
+ object (self)
+  inherit NCicUnifHint.status
+  inherit NCicCoercion.status
+  inherit NCicLibrary.status
+  method set_rstatus o =
+   ((self#set_unifhint_status (o :> NCicUnifHint.status))
+         #set_coercion_status (o :> NCicCoercion.status))
+         #set_library_status  (o :> NCicLibrary.status)
  end
 
 type sstatus = status
@@ -32,10 +44,20 @@ module Serializer =
     status 
  end
 
-class dumpable_status =
+class type ctdumpable_status =
+ object ('self)
+  inherit status
+  method dump: Serializer.obj list
+  method set_dump: Serializer.obj list -> 'self
+  method set_dumpable_status: ctdumpable_status -> 'self
+ end
+
+class dumpable_status : ctdumpable_status =
  object
   inherit status
   val dump = ([] : Serializer.obj list)
   method dump = dump
   method set_dump v = {< dump = v >}
+  method set_dumpable_status o =
+   {< dump = o#dump >}#set_rstatus (o :> status)
  end