aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
multi_aliases: DisambiguateTypes.multiple_environment;
moo_content_rev: GrafiteMarshal.moo;
+ metadata: LibraryNoDb.metadata list;
proof_status: proof_status; (** logical status *)
options: options;
objects: UriManager.uri list; (** in-scope objects *)
(** list is not reversed, head command will be the first emitted *)
val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
-val add_moo_metadata: GrafiteAst.metadata list -> status -> status
+val add_metadata: LibraryNoDb.metadata list -> status -> status
val get_option : status -> string -> option_value
val get_string_option : status -> string -> string