]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nRstatus.mli
Objects are now used to represent also the tactic status.
[helm.git] / helm / software / components / ng_refiner / nRstatus.mli
index 522d7e901b396d373db8b98674ba5eae9f690954..7fde1b74733c5be2348432daf060eb5ce29a0a31 100644 (file)
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
 class status :
- object
+ object ('self)
   inherit NCicUnifHint.status
   inherit NCicCoercion.status
   inherit NCicLibrary.status
+  method set_rstatus: status -> 'self
  end
 
 module Serializer:
@@ -29,4 +30,5 @@ class dumpable_status :
   inherit status
   method dump: Serializer.obj list
   method set_dump: Serializer.obj list -> 'self
+  method set_dumpable_status: dumpable_status -> 'self
  end