Module `Coqargs`Source

Sourceval default_toplevel : Names.DirPath.t

Sourcetype native_compiler = Coq_config.native_compiler =

| NativeOff
| NativeOn of {
1. ondemand : bool;
}

Sourcetype top =

| TopLogical of Names.DirPath.t
| TopPhysical of string

Sourcetype option_command =

| OptionSet of string option
| OptionUnset
| OptionAppend of string

Sourcetype injection_command =

| OptionInjection of Goptions.option_name * option_command
(*
Set flags or options before the initial state is ready.
*)
| RequireInjection of string * string option * Lib.export_flag option
(*
Require libraries before the initial state is ready. Parameters follow Library, that is to say, lib,prefix,import_export means require library lib from optional prefix and import_export if Some Lib.Import/Some Lib.Export is used.
*)
| WarnNoNative of string
(*
Used so that "-w -native-compiler-disabled -native-compiler yes" does not cause a warning. The native option must be processed before injections (because it affects require), so the instruction to emit a message is separated.
*)
| WarnNativeDeprecated
(*
Used so that "-w -native-compiler-deprecated-option -native-compiler FLAG" does not cause a warning, similarly to above.
*)

Sourcetype coqargs_logic_config = {

impredicative_set : bool;
indices_matter : bool;
type_in_type : bool;
toplevel_name : top;

}

Sourcetype coqargs_config = {

logic : coqargs_logic_config;
rcfile : string option;
coqlib : string option;
enable_VM : bool;
native_compiler : native_compiler;
native_output_dir : CUnix.physical_path;
native_include_dirs : CUnix.physical_path list;
time : bool;
print_emacs : bool;

}

Sourcetype coqargs_pre = {

boot : bool;
load_init : bool;
load_rcfile : bool;
ml_includes : CUnix.physical_path list;
vo_includes : Loadpath.vo_path list;
load_vernacular_list : (string * bool) list;
injections : injection_command list;

}

Sourcetype coqargs_query =

| PrintWhere
| PrintConfig
| PrintVersion
| PrintMachineReadableVersion
| PrintHelp of Boot.Usage.specific_usage

Sourcetype coqargs_main =

| Queries of coqargs_query list
| Run

Sourcetype coqargs_post = {

memory_stat : bool;

}

Sourcetype t = {

config : coqargs_config;
pre : coqargs_pre;
main : coqargs_main;
post : coqargs_post;

}

Sourceval default : t

Source

val parse_args : 
  usage:Boot.Usage.specific_usage ->
  init:t ->
  string list ->
  t * string list

Sourceval injection_commands : t -> injection_command list

Sourceval dirpath_of_top : top -> Names.DirPath.t

Sourceval get_int : opt:string -> string -> int

Sourceval get_int_opt : opt:string -> string -> int option

Sourceval get_bool : opt:string -> string -> bool

Sourceval get_float : opt:string -> string -> float

Sourceval error_missing_arg : string -> 'a

Sourceval error_wrong_arg : string -> 'a

Sourceval set_option : (Goptions.option_name * option_command) -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.sysinit/Coqargs/index.html

Module `Coqargs`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.sysinit/Coqargs/index.html

Module CoqargsSource

Module `Coqargs`Source