From aaedd6050f1fb78c1354e4a3a1431c9de3727127 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 21 Dec 2011 23:22:20 +0000
Subject: sequel of previous commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14842 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/goptions.mli | 22 +++-------------------
 1 file changed, 3 insertions(+), 19 deletions(-)

(limited to 'library/goptions.mli')

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
-- 
cgit v1.2.3