val no_options : 'a StringMap.t
type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
val no_options : 'a StringMap.t
type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
- moo_content_rev: ast_command list;
- proof_status: proof_status;
+ aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ multi_aliases: DisambiguateTypes.multiple_environment;
+ moo_content_rev: moo;
+ proof_status: proof_status; (** logical status *)
}
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 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