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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Global options of the system. *)
(** WARNING: don't add new entries to this file!
This file is own its way to deprecation in favor of a purely
functional state, but meanwhile it will contain options that are
truly global to the system such as [compat] or [debug]
If you are thinking about adding a global flag, well, just
don't. First of all, options make testins exponentially more
expensive, due to the growth of flag combinations. So please make
some effort in order for your idea to work in a configuration-free
manner.
If you absolutely must pass an option to your new system, then do
so as a functional argument so flags are exposed to unit
testing. Then, register such parameters with the proper
state-handling mechanism of the top-level subsystem of Coq.
*)
(** Command-line flags *)
val boot : bool ref
(** Set by coqtop to tell the kernel to output to the aux file; will
be eventually removed by cleanups such as PR#1103 *)
val record_aux_file : bool 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 *)
val async_proofs_worker_id : string ref
val async_proofs_is_worker : unit -> bool
(** Debug flags *)
val debug : bool ref
val in_debugger : bool ref
val in_toplevel : bool ref
val profile : bool
(* 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
type compat_version = V8_6 | V8_7 | 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
(* 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
(** Global polymorphic inductive cumulativity flag. *)
val make_polymorphic_inductive_cumulativity : bool -> unit
val is_polymorphic_inductive_cumulativity : unit -> bool
val warn : bool ref
val make_warn : bool -> unit
val if_warn : ('a -> unit) -> 'a -> unit
(** [with_modified_ref r nf f x] Temporarily modify a reference in the
call to [f x] . Be very careful with these functions, it is very
easy to fall in the typical problem with effects:
with_modified_ref r nf f x y != with_modified_ref r nf (f x) y
*)
val with_modified_ref : 'c ref -> ('c -> 'c) -> ('a -> 'b) -> 'a -> 'b
(** 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
(** Level of inlining during a functor application *)
val set_inline_level : int -> unit
val get_inline_level : unit -> int
val default_inline_level : int
(** When producing vo objects, also compile the native-code version *)
val output_native_objects : bool ref
(** Print the mod uid associated to a vo file by the native compiler *)
val print_mod_uid : bool ref
val profile_ltac : bool ref
val profile_ltac_cutoff : float ref
|
