| Intermediate of Cic.metasenv
type ng_status =
- | ProofMode of NTactics.tac_status
+ | ProofMode of NTacStatus.tac_status
| CommandMode of LexiconEngine.status
type status = {
proof_status: proof_status;
objects: UriManager.uri list;
coercions: CoercDb.coerc_db;
- universe:Universe.universe;
+ automation_cache:AutomationCache.cache;
baseuri: string;
ng_status: ng_status;
}