From 9e89bf92ee52004eaf4fc6491c623b9b7db1da2a Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 18 Nov 2011 20:30:27 +0000
Subject: Adding the type infrastructure to handle properly API management of
 options

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14689 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 2 +-
 toplevel/vernacexpr.ml    | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cd30eaf5ca..88b78a633f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -997,7 +997,7 @@ let vernac_set_opacity local str =
 
 let vernac_set_option locality key = function
   | StringValue s -> set_string_option_value_gen locality key s
-  | IntValue n -> set_int_option_value_gen locality key (Some n)
+  | IntValue n -> set_int_option_value_gen locality key n
   | BoolValue b -> set_bool_option_value_gen locality key b
 
 let vernac_unset_option locality key =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 32ea70baf2..bae6cfcdd9 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -134,10 +134,10 @@ 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 =
-  | StringValue of string
-  | IntValue of int
+type option_value = Goptions.option_value =
   | BoolValue of bool
+  | IntValue of int option
+  | StringValue of string
 
 type option_ref_value =
   | StringRefValue of string
-- 
cgit v1.2.3