+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}}
+ | CommandMode _ -> CommandMode e}
+;;
+
+let get_rstatus x = (get_estatus x).NEstatus.rstatus;;
+
+let get_hstatus x = (get_rstatus x).NRstatus.uhint_db;;
+
+let get_library_db x = (get_rstatus x).NRstatus.library_db;;
+
+let get_dump x = (get_rstatus x).NRstatus.dump;;
+
+let set_rstatus h x =
+ let estatus = get_estatus x in
+ set_estatus { estatus with NEstatus.rstatus = h } x
+;;
+
+let set_hstatus h x =
+ let rstatus = get_rstatus x in
+ set_rstatus { rstatus with NRstatus.uhint_db = h} x
+;;
+
+let set_library_db h x =
+ let rstatus = get_rstatus x in
+ set_rstatus { rstatus with NRstatus.library_db = h} x
+;;
+
+let set_dump h x =
+ let estatus = get_estatus x in
+ set_estatus
+ { estatus with NEstatus.rstatus =
+ { estatus.NEstatus.rstatus with
+ NRstatus.dump = h}}
+ x
+;;
+