blob: 0b00ac13c26a34a21c972e63b89eaae1244123de (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** Global options of the system. *)
(** Command-line flags *)
val boot : bool ref
val load_init : bool ref
val batch_mode : bool ref
type compilation_mode = BuildVo | BuildVio | Vio2Vo
val compilation_mode : compilation_mode ref
val compilation_output_name : string option ref
(* Flag set when the test-suite is called. Its only effect to display
verbose information for `Fail` *)
val test_mode : bool ref
(** Async-related flags *)
type async_proofs = APoff | APonLazy | APon
val async_proofs_mode : async_proofs ref
type cache = Force
val async_proofs_cache : cache option ref
val async_proofs_n_workers : int ref
val async_proofs_n_tacworkers : int ref
val async_proofs_private_flags : string option ref
val async_proofs_is_worker : unit -> bool
val async_proofs_is_master : unit -> bool
val async_proofs_full : bool ref
val async_proofs_never_reopen_branch : bool ref
val async_proofs_flags_for_workers : string list ref
val async_proofs_worker_id : string ref
type priority = Low | High
val async_proofs_worker_priority : priority ref
val string_of_priority : priority -> string
val priority_of_string : string -> priority
type tac_error_filter = [ `None | `Only of string list | `All ]
val async_proofs_tac_error_resilience : tac_error_filter ref
val async_proofs_cmd_error_resilience : bool ref
val async_proofs_delegation_threshold : float ref
val debug : bool ref
val in_debugger : bool ref
val in_toplevel : bool ref
val profile : bool
(* Legacy flags *)
(* -emacs option: printing includes emacs tags, will affect stm caching. *)
val print_emacs : bool ref
(* -xml option: xml hooks will be called *)
val xml_export : bool ref
(* -ide_slave: printing will be more verbose, will affect stm caching *)
val ide_slave : bool ref
val ideslave_coqtop_flags : string option ref
(* -time option: every command will be wrapped with `Time` *)
val time : bool ref
(* development flag to detect race conditions, it should go away. *)
val we_are_parsing : bool ref
(* Set Printing All flag. For some reason it is a global flag *)
val raw_print : bool ref
(* Univ print flag, never set anywere. Maybe should belong to Univ? *)
val univ_print : bool ref
type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
val compat_version : compat_version ref
val version_compare : compat_version -> compat_version -> int
val version_strictly_greater : compat_version -> bool
val version_less_or_equal : compat_version -> bool
val pr_version : compat_version -> string
(* Beautify command line flags, should move to printing? *)
val beautify : bool ref
val beautify_file : bool ref
(* Coq quiet mode. Note that normal mode is called "verbose" here,
whereas [quiet] supresses normal output such as goals in coqtop *)
val quiet : bool ref
val silently : ('a -> 'b) -> 'a -> 'b
val verbosely : ('a -> 'b) -> 'a -> 'b
val if_silent : ('a -> unit) -> 'a -> unit
val if_verbose : ('a -> unit) -> 'a -> unit
(* Deprecated *)
val make_silent : bool -> unit
[@@ocaml.deprecated "Please use Flags.quiet"]
val is_silent : unit -> bool
[@@ocaml.deprecated "Please use Flags.quiet"]
val is_verbose : unit -> bool
[@@ocaml.deprecated "Please use Flags.quiet"]
(* Miscellaneus flags for vernac *)
val make_auto_intros : bool -> unit
val is_auto_intros : unit -> bool
val program_mode : bool ref
val is_program_mode : unit -> bool
(** Global universe polymorphism flag. *)
val make_universe_polymorphism : bool -> unit
val is_universe_polymorphism : unit -> bool
(** Local universe polymorphism flag. *)
val make_polymorphic_flag : bool -> unit
val use_polymorphic_flag : unit -> bool
val warn : bool ref
val make_warn : bool -> unit
val if_warn : ('a -> unit) -> 'a -> unit
(** Temporarily activate an option (to activate option [o] on [f x y z],
use [with_option o (f x y) z]) *)
val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
(** As [with_option], but on several flags. *)
val with_options : bool ref list -> ('a -> 'b) -> 'a -> 'b
(** Temporarily deactivate an option *)
val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
(** Temporarily extends the reference to a list *)
val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b
(** Options for external tools *)
(** Returns string format for default browser to use from Coq or CoqIDE *)
val browser_cmd_fmt : string
val is_standard_doc_url : string -> bool
(** Options for specifying where coq librairies reside *)
val coqlib_spec : bool ref
val coqlib : string ref
(** Options for specifying where OCaml binaries reside *)
val ocamlfind_spec : bool ref
val ocamlfind : string ref
val camlp4bin_spec : bool ref
val camlp4bin : string ref
(** Level of inlining during a functor application *)
val set_inline_level : int -> unit
val get_inline_level : unit -> int
val default_inline_level : int
(** Native code compilation for conversion and normalization *)
val native_compiler : bool ref
(** Print the mod uid associated to a vo file by the native compiler *)
val print_mod_uid : bool ref
val tactic_context_compat : bool ref
(** Set to [true] to trigger the compatibility bugged context matching (old
context vs. appcontext) is set. *)
val profile_ltac : bool ref
val profile_ltac_cutoff : float ref
(** Dump the bytecode after compilation (for debugging purposes) *)
val dump_bytecode : bool ref
val set_dump_bytecode : bool -> unit
val get_dump_bytecode : unit -> bool
|
