Module Goptions

This module manages customization parameters at the vernacular level

type option_name = string list
type option_locality =
| OptDefault
| OptLocal
| OptExport
| OptGlobal
Tables.
module MakeStringTable : functor (A : sig ... end) -> sig ... end
module MakeRefTable : functor (A : sig ... end) -> sig ... end
Options.
type 'a option_sig = {
optdepr : bool;

whether the option is DEPRECATED

optkey : option_name;

the low-level name of this option

optread : unit -> 'a;
optwrite : 'a -> unit;
}
val declare_int_option : ?⁠preprocess:(int option -> int option) -> int option option_sig -> unit
val declare_bool_option : ?⁠preprocess:(bool -> bool) -> bool option_sig -> unit
val declare_string_option : ?⁠preprocess:(string -> string) -> string option_sig -> unit
val declare_stringopt_option : ?⁠preprocess:(string option -> string option) -> string option option_sig -> unit
type 'a opt_decl = depr:bool -> key:option_name -> 'a

Helpers to declare a reference controlled by an option. Read-only as to avoid races.

val declare_int_option_and_ref : (value:int -> unit -> int) opt_decl
val declare_intopt_option_and_ref : (unit -> int option) opt_decl
val declare_nat_option_and_ref : (value:int -> unit -> int) opt_decl
val declare_bool_option_and_ref : (value:bool -> unit -> bool) opt_decl
val declare_string_option_and_ref : (value:string -> unit -> string) opt_decl
val declare_stringopt_option_and_ref : (unit -> string option) opt_decl
val declare_interpreted_string_option_and_ref : (value:'a -> (string -> 'a) -> ('a -> string) -> unit -> 'a) opt_decl
Special functions supposed to be used only in vernacentries.ml
module OptionMap : CSig.MapS with type key = option_name
type 'a table_of_A = {
add : Environ.env -> 'a -> unit;
remove : Environ.env -> 'a -> unit;
mem : Environ.env -> 'a -> unit;
print : unit -> unit;
}
val get_string_table : option_name -> string table_of_A
val get_ref_table : option_name -> Libnames.qualid table_of_A
val set_int_option_value_gen : ?⁠locality:option_locality -> option_name -> int option -> unit

The first argument is a locality flag.

val set_bool_option_value_gen : ?⁠locality:option_locality -> option_name -> bool -> unit
val set_string_option_value_gen : ?⁠locality:option_locality -> option_name -> string -> unit
val set_string_option_append_value_gen : ?⁠locality:option_locality -> option_name -> string -> unit
val unset_option_value_gen : ?⁠locality:option_locality -> option_name -> unit
val set_int_option_value : option_name -> int option -> unit
val set_bool_option_value : option_name -> bool -> unit
val set_string_option_value : option_name -> string -> unit
val print_option_value : option_name -> unit
type option_value =
| BoolValue of bool
| IntValue of int option
| StringValue of string
| StringOptValue of string option
type table_value =
| StringRefValue of string
| QualidRefValue of Libnames.qualid
val set_option_value : ?⁠locality:option_locality -> ('a -> option_value -> option_value) -> option_name -> 'a -> unit

set_option_value ?locality f name v sets name to the result of applying f to v and name's current value. Use for behaviour depending on the type of the option, eg erroring when 'a doesn't match it. Changing the type will result in errors later so don't do that.

type option_state = {
opt_depr : bool;
opt_value : option_value;
}

Summary of an option status

val get_tables : unit -> option_state OptionMap.t
val print_tables : unit -> Pp.t
type iter_table_aux = {
aux : a. 'a table_of_A -> Environ.env -> 'a -> unit;
}
val iter_table : iter_table_aux -> option_name -> table_value list -> unit
val error_undeclared_key : option_name -> 'a