val no_options : 'a StringMap.t
type status = {
- aliases : DisambiguateTypes.environment;
- moo_content_rev : string list;
- proof_status : proof_status;
- options : options;
- objects : (UriManager.uri * string) list;
+ aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ moo_content_rev: string list;(*CSC: GrafiteAst.command list would be better *)
+ proof_status: proof_status;
+ options: options;
+ objects: (UriManager.uri * string) list; (** in-scope objects, with paths *)
+ notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
}
val dump_status : status -> unit