diff options
| -rw-r--r-- | library/goptions.ml | 18 | ||||
| -rw-r--r-- | library/goptions.mli | 22 | ||||
| -rw-r--r-- | toplevel/interface.mli | 6 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
4 files changed, 11 insertions, 37 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index f5100a14a..90c8728c1 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -17,28 +17,18 @@ open Term open Nametab open Mod_subst +open Goptionstyp + +type option_name = Goptionstyp.option_name + (****************************************************************************) (* 0- Common things *) -type option_name = string list - let nickname table = String.concat " " table let error_undeclared_key key = error ((nickname key)^": no table or option of this type") -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; -} - (****************************************************************************) (* 1- Tables *) 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 diff --git a/toplevel/interface.mli b/toplevel/interface.mli index 8aa6c9200..e1410f5bc 100644 --- a/toplevel/interface.mli +++ b/toplevel/interface.mli @@ -43,15 +43,15 @@ type goals = { type hint = (string * string) list (** A list of tactics applicable and their appearance *) -type option_name = Goptions.option_name +type option_name = Goptionstyp.option_name -type option_value = Goptions.option_value = +type option_value = Goptionstyp.option_value = | BoolValue of bool | IntValue of int option | StringValue of string (** Summary of an option status *) -type option_state = Goptions.option_state = { +type option_state = Goptionstyp.option_state = { opt_sync : bool; (** Whether an option is synchronous *) opt_depr : bool; diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 517d77e9d..850bc111a 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -134,7 +134,7 @@ type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type infer_flag = bool (* true = try to Infer record; false = nothing *) type full_locality_flag = bool option (* true = Local; false = Global *) -type option_value = Goptions.option_value = +type option_value = Goptionstyp.option_value = | BoolValue of bool | IntValue of int option | StringValue of string |