diff options
Diffstat (limited to 'library/goptions.mli')
-rw-r--r-- | library/goptions.mli | 26 |
1 files changed, 18 insertions, 8 deletions
diff --git a/library/goptions.mli b/library/goptions.mli index 1b51a7f7..1c44f890 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -44,14 +44,10 @@ (synchronous = consistent with the resetting commands) *) open Pp -open Util -open Names open Libnames -open Term -open Nametab open Mod_subst -type option_name = Goptionstyp.option_name +type option_name = string list (** {6 Tables. } *) @@ -90,6 +86,7 @@ module MakeRefTable : functor (A : sig type t + val compare : t -> t -> int val encode : reference -> t val subst : substitution -> t -> t val printer : t -> std_ppcmds @@ -164,7 +161,20 @@ val set_string_option_value : option_name -> string -> unit val print_option_value : option_name -> unit -val get_tables : unit -> Goptionstyp.option_state OptionMap.t -val print_tables : unit -> unit +type option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + +(** Summary of an option status *) +type option_state = { + opt_sync : bool; + opt_depr : bool; + opt_name : string; + opt_value : option_value; +} + +val get_tables : unit -> option_state OptionMap.t +val print_tables : unit -> std_ppcmds val error_undeclared_key : option_name -> 'a |