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.ml | 18 ++++--------------
 1 file changed, 4 insertions(+), 14 deletions(-)

(limited to 'library/goptions.ml')

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