package coq

  1. Overview
  2. Docs
package coq
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 = Coq_config.native_compiler =
  1. | NativeOff
  2. | NativeOn of {
    1. ondemand : bool;
    }
type coqargs_logic_config = {
  1. impredicative_set : Declarations.set_predicativity;
  2. indices_matter : bool;
  3. toplevel_name : Stm.interactive_top;
}
type coqargs_config = {
  1. logic : coqargs_logic_config;
  2. rcfile : string option;
  3. coqlib : string option;
  4. color : color;
  5. enable_VM : bool;
  6. native_compiler : native_compiler;
  7. native_output_dir : CUnix.physical_path;
  8. native_include_dirs : CUnix.physical_path list;
  9. stm_flags : Stm.AsyncOpts.stm_opt;
  10. debug : bool;
  11. time : bool;
  12. print_emacs : bool;
}
type coqargs_pre = {
  1. boot : bool;
  2. load_init : bool;
  3. load_rcfile : bool;
  4. ml_includes : CUnix.physical_path list;
  5. vo_includes : Loadpath.vo_path list;
  6. load_vernacular_list : (string * bool) list;
  7. injections : Stm.injection_command list;
  8. inputstate : string option;
}
type coqargs_query =
  1. | PrintTags
  2. | PrintWhere
  3. | PrintConfig
  4. | PrintVersion
  5. | PrintMachineReadableVersion
  6. | PrintHelp of Usage.specific_usage
type coqargs_main =
  1. | Queries of coqargs_query list
  2. | Run
type coqargs_post = {
  1. memory_stat : bool;
  2. output_context : bool;
}
type t = {
  1. config : coqargs_config;
  2. pre : coqargs_pre;
  3. main : coqargs_main;
  4. post : coqargs_post;
}
val default : t
val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list
val error_wrong_arg : string -> unit
val injection_commands : t -> Stm.injection_command list
val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list