type options = option_value StringMap.t
val no_options : 'a StringMap.t
-type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command
type moo = ast_command list * GrafiteAst.metadata list (** <moo, metadata> *)
type status = {
proof_status: proof_status; (** logical status *)
options: options;
objects: (UriManager.uri * string) list; (** in-scope objects, with paths *)
+ coercions: UriManager.uri list; (** defined coercions *)
notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
}