From aaedd6050f1fb78c1354e4a3a1431c9de3727127 Mon Sep 17 00:00:00 2001
From: letouzey
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.ml    | 18 ++++--------------
 library/goptions.mli   | 22 +++-------------------
 toplevel/interface.mli |  6 +++---
 toplevel/vernacexpr.ml |  2 +-
 4 files changed, 11 insertions(+), 37 deletions(-)

diff --git a/library/goptions.ml b/library/goptions.ml
index f5100a14a9..90c8728c11 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 685af53da9..d25c1202f3 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 8aa6c9200d..e1410f5bc9 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 517d77e9db..850bc111af 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
-- 
cgit v1.2.3