diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-24 19:12:48 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-24 19:12:48 +0000 |
| commit | ecd2f83848ab06048d67189972e92657bffcc92d (patch) | |
| tree | 0bd4a599253ae6a3d68372d0d6650f2d99cb8b79 /library/goptions.mli | |
| parent | 2ed4b1e88e3e304c5146d74124d7057ac62c59a2 (diff) | |
Added a function to inspect current option state.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/goptions.mli')
| -rw-r--r-- | library/goptions.mli | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/library/goptions.mli b/library/goptions.mli index 37c03f1bf..685af53da 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -140,18 +140,20 @@ val declare_string_option: string option_sig -> string write_function (** {6 Special functions supposed to be used only in vernacentries.ml } *) -type 'a option_state = { - opt_sync : bool; - opt_name : string; - opt_key : option_name; - opt_value : 'a; -} +module OptionMap : Map.S with type key = option_name type option_value = | BoolValue of bool | IntValue of int option | StringValue of string +type option_state = { + opt_sync : bool; + opt_depr : bool; + opt_name : string; + opt_value : option_value; +} + val get_string_table : option_name -> < add : string -> unit; @@ -179,5 +181,6 @@ val set_string_option_value : option_name -> string -> unit val print_option_value : option_name -> unit +val get_tables : unit -> option_state OptionMap.t val print_tables : unit -> unit |