Module Coqtop

Definition of custom toplevels. init is used to do custom command line argument parsing. run launches a custom toplevel.

type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list
type custom_toplevel = {
init : init_fn;
run : opts:Coqargs.t -> state:Vernac.State.t -> unit;
opts : Coqargs.t;
}
val init_toplevel : help:(unit -> unit) -> init:Coqargs.t -> init_fn -> string list -> Coqargs.t * string list

init_toplevel ~help ~init custom_init arg_list Common Coq initialization and argument parsing

val coqtop_toplevel : custom_toplevel
val start_coq : custom_toplevel -> unit