Imported Upstream version 8.5~beta1+dfsg

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