sequel of previous commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14842 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 14 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                                                                *)