package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type option_name = string list
type option_locality =
  1. | OptDefault
  2. | OptLocal
  3. | OptExport
  4. | OptGlobal
module MakeStringTable (A : sig ... end) : sig ... end
module MakeRefTable (A : sig ... end) : sig ... end
type !'a option_sig = {
  1. optdepr : bool;
  2. optkey : option_name;
  3. optread : unit -> 'a;
  4. 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
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
module OptionMap : sig ... end
type !'a table_of_A = {
  1. add : Environ.env -> 'a -> unit;
  2. remove : Environ.env -> 'a -> unit;
  3. mem : Environ.env -> 'a -> unit;
  4. 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
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 =
  1. | BoolValue of bool
  2. | IntValue of int option
  3. | StringValue of string
  4. | StringOptValue of string option
type table_value =
  1. | StringRefValue of string
  2. | QualidRefValue of Libnames.qualid
val set_option_value : ?locality:option_locality -> ('a -> option_value -> option_value) -> option_name -> 'a -> unit
type option_state = {
  1. opt_depr : bool;
  2. opt_value : option_value;
}
val get_tables : unit -> option_state OptionMap.t
val print_tables : unit -> Pp.t
type iter_table_aux = {
  1. 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