X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteTypes.ml;h=82dae3d996a719e30de7ee97ff9674b7ca6cd606;hb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;hp=6033be8c2c09cce599a63919822a32c75e930413;hpb=a9e037fe189335607ab5d10523c836d8c7717245;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 6033be8c2..82dae3d99 100644
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -46,7 +46,7 @@ type proof_status =
 
 type ng_status =
   | ProofMode of NTacStatus.tac_status
-  | CommandMode of NEstatus.extra_status
+  | CommandMode of NEstatus.status
 
 type status = {
   moo_content_rev: GrafiteMarshal.moo;
@@ -58,26 +58,6 @@ type status = {
   ng_status: ng_status;
 }
 
-let get_lexicon x = 
-  match x.ng_status with
-  | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.lstatus
-  | CommandMode e -> e.NEstatus.lstatus
-;;
- 
-let set_lexicon new_lexicon_status new_grafite_status = 
-  { new_grafite_status with ng_status =
-   match new_grafite_status.ng_status with
-   | CommandMode estatus -> 
-      CommandMode 
-        { estatus with NEstatus.lstatus = new_lexicon_status }
-   | ProofMode t -> 
-       ProofMode 
-        { t with NTacStatus.istatus = 
-          { t.NTacStatus.istatus with NTacStatus.estatus = 
-            { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.lstatus =
-               new_lexicon_status }}}}
-;; 
-
 let get_estatus x = 
   match x.ng_status with
   | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus
@@ -94,13 +74,6 @@ let set_estatus e x =
     | CommandMode _ -> CommandMode e}
 ;;
 
-let get_dstatus x = (get_estatus x).NEstatus.rstatus;;
-
-let set_dstatus h x =
- let estatus = get_estatus x in
-  set_estatus { estatus with NEstatus.rstatus = h } x
-;;
-
 let get_current_proof status =
   match status.proof_status with
   | Incomplete_proof { proof = p } -> p