(* 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;
objects: UriManager.uri list;
coercions: CoercDb.coerc_db;
- universe:Universe.universe;
+ automation_cache:AutomationCache.cache;
baseuri: string;
- ng_status: NTactics.tac_status option;
+ ng_status: ng_status;
}
let get_current_proof status =