package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type color = [
  1. | `AUTO
  2. | `EMACS
  3. | `OFF
  4. | `ON
]
val default_toplevel : Names.DirPath.t
type native_compiler =
  1. | NativeOff
  2. | NativeOn of {
    1. ondemand : bool;
    }
type option_command =
  1. | OptionSet of string option
  2. | OptionUnset
type t = {
  1. load_init : bool;
  2. load_rcfile : bool;
  3. rcfile : string option;
  4. ml_includes : Mltop.coq_path list;
  5. vo_includes : Mltop.coq_path list;
  6. vo_requires : (string * string option * bool option) list;
  7. toplevel_name : Stm.interactive_top;
  8. load_vernacular_list : (string * bool) list;
  9. batch : bool;
  10. color : color;
  11. impredicative_set : Declarations.set_predicativity;
  12. indices_matter : bool;
  13. enable_VM : bool;
  14. native_compiler : native_compiler;
  15. allow_sprop : bool;
  16. cumulative_sprop : bool;
  17. set_options : (Goptions.option_name * option_command) list;
  18. stm_flags : Stm.AsyncOpts.stm_opt;
  19. debug : bool;
  20. diffs_set : bool;
  21. time : bool;
  22. filter_opts : bool;
  23. memory_stat : bool;
  24. print_tags : bool;
  25. print_where : bool;
  26. print_config : bool;
  27. output_context : bool;
  28. print_emacs : bool;
  29. inputstate : string option;
}
val default : t
val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list
val exitcode : t -> int
val require_libs : t -> (string * string option * bool option) list
val build_load_path : t -> Mltop.coq_path list
OCaml

Innovation. Community. Security.