diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-21 23:22:20 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-21 23:22:20 +0000 |
| commit | aaedd6050f1fb78c1354e4a3a1431c9de3727127 (patch) | |
| tree | 63dcde29a43b276d4aa785c14853aa5c88b65c0a /library/goptions.mli | |
| parent | a2c18c0369de7ca302ad398b348ab429fe8f3fbe (diff) | |
sequel of previous commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14842 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/goptions.mli')
| -rw-r--r-- | library/goptions.mli | 22 |
1 files changed, 3 insertions, 19 deletions
diff --git a/library/goptions.mli b/library/goptions.mli index 685af53da..d25c1202f 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -51,12 +51,7 @@ open Term open Nametab open Mod_subst -(** {6 Things common to tables and options. } *) - -(** The type of table/option keys *) -type option_name = string list - -val error_undeclared_key : option_name -> 'a +type option_name = Goptionstyp.option_name (** {6 Tables. } *) @@ -142,18 +137,6 @@ val declare_string_option: string option_sig -> string write_function 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; @@ -181,6 +164,7 @@ 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 get_tables : unit -> Goptionstyp.option_state OptionMap.t val print_tables : unit -> unit +val error_undeclared_key : option_name -> 'a |