package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
type async_flags = {
  1. enable_async : string option;
  2. deep_edits : bool;
  3. async_workers : int;
  4. error_recovery : bool;
}

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 : Format.formatter -> Feedback.feedback -> unit;
    (*

    callback to handle async feedback

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

    callback to load findlib plugins

    *)
  3. debug : bool;
    (*

    Enable Coq Debug mode

    *)
  4. set_impredicative_set : bool;
    (*

    Enable -impredicative-set option in Coq (default=false)

    *)
  5. allow_sprop : bool;
    (*

    allow using the proof irrelevant SProp sort (default=true)

    *)
  6. indices_matter : bool;
    (*

    Levels of indices (and nonuniform parameters) contribute to the level of inductives

    *)
  7. ml_path : string list;
  8. vo_path : Loadpath.vo_path list;
    (*

    From -R and -Q options usually

    *)
}
val coq_init : coq_opts -> Format.formatter -> unit

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

val update_fb_handler : pp_feed:(Format.formatter -> Feedback.feedback -> unit) -> Format.formatter -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct