type options = option_value StringMap.t
val no_options : 'a StringMap.t
-type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command
-type moo = ast_command list * GrafiteAst.metadata list (** <moo, metadata> *)
-
type status = {
aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
multi_aliases: DisambiguateTypes.multiple_environment;
- moo_content_rev: moo;
+ moo_content_rev: GrafiteMarshal.moo;
proof_status: proof_status; (** logical status *)
options: options;
objects: (UriManager.uri * string) list; (** in-scope objects, with paths *)
val set_metasenv: Cic.metasenv -> status -> status
(** list is not reversed, head command will be the first emitted *)
-val add_moo_content: ast_command list -> status -> status
+val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
val add_moo_metadata: GrafiteAst.metadata list -> status -> status
val dump_status : status -> unit