Flags
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 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
Flag to indicate that .vos files should be loaded for dependencies instead of .vo files. Used by -vos and -vok options.
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
Temporarily activate an option (to activate option o
on f x y z
, use with_option o (f x y) z
)
As with_option
, but on several flags.
Temporarily extends the reference to a list