(* Status in which the proof could be while it is being processed by the
* engine. No status entering/exiting the engine could be in it. *)
+type ng_status =
+ | ProofMode of NTacStatus.tac_status
+ | CommandMode of LexiconEngine.status
+
type status = {
moo_content_rev: GrafiteMarshal.moo;
proof_status: proof_status;
coercions: CoercDb.coerc_db;
universe:Universe.universe;
baseuri: string;
+ ng_status: ng_status;
}
let get_current_proof status =