Module Sertop_init

type async_flags = {
  1. enable_async : string option;
  2. deep_edits : bool;
  3. async_workers : int;
}

SerAPI flags for asynchronous processing

val process_stm_flags : async_flags -> Stm.AsyncOpts.stm_opt

process_stm_flags flags transforms SerAPI flags into Coq flags

type coq_opts = {
  1. fb_handler : Feedback.feedback -> unit;
    (*

    callback to handle async feedback

    *)
  2. ml_load : (string -> unit) option;
    (*

    callback to load cma/cmo files

    *)
  3. debug : bool;
    (*

    Enable Coq Debug mode

    *)
}
val coq_init : coq_opts -> unit

coq_init opts Initialize Coq. This doesn't create a Proof Document.