+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 set_coercions db new_grafite_status =
+ { new_grafite_status with ng_status =
+ match new_grafite_status.ng_status with
+ | CommandMode estatus ->
+ CommandMode
+ { estatus with NEstatus.rstatus =
+ { estatus.NEstatus.rstatus with NRstatus.coerc_db = db }}
+ | ProofMode t ->
+ ProofMode
+ { t with NTacStatus.istatus =
+ { t.NTacStatus.istatus with NTacStatus.estatus =
+ { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.rstatus =
+ { t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.rstatus with NRstatus.coerc_db = db
+ }}}}}
+;;
+
+let get_estatus x =
+ match x.ng_status with
+ | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus
+ | CommandMode e -> e
+;;
+