]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/nEstatus.mli
Objects are now used to represent also the tactic status.
[helm.git] / helm / software / components / grafite_parser / nEstatus.mli
index 2c3acc751bd045ceeb8627a8ca1eea77280ce420..e77f4e5665cd1088de8fe0010a75b0560911dca9 100644 (file)
@@ -12,7 +12,8 @@
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
 class status :
- object
+ object ('self)
   inherit LexiconEngine.status
   inherit NRstatus.dumpable_status
+  method set_estatus: status -> 'self
  end