Objects are now used to represent also the tactic status.

[helm.git] / helm / software / components / grafite_engine / grafiteTypes.ml

diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 82dae3d996a719e30de7ee97ff9674b7ca6cd606..5d0ce025deb6cefd749dc3c2372dd575200538b7 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -60,17 +60,14 @@ type status = {
 
 let get_estatus x = 
   match x.ng_status with
-  | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus
+  | ProofMode t -> (t :> NEstatus.status)
   | CommandMode e -> e
 ;;
 
 let set_estatus e x =
  { x with ng_status =
    match x.ng_status with
-      ProofMode t ->
-       ProofMode
-        {t with NTacStatus.istatus =
-         {t.NTacStatus.istatus with NTacStatus.estatus = e}}
+      ProofMode t -> ProofMode t#set_estatus e
     | CommandMode _ -> CommandMode e}
 ;;