aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/goptions.mli
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-18 20:30:27 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-18 20:30:27 +0000
commit9e89bf92ee52004eaf4fc6491c623b9b7db1da2a (patch)
tree00b8a22e7b319059b14a5be43c0b580a17624a43 /library/goptions.mli
parent2d3430f3a49d844fdbff5db8d706b372ffec7a17 (diff)
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
Diffstat (limited to 'library/goptions.mli')
-rw-r--r--library/goptions.mli12
1 files changed, 12 insertions, 0 deletions
diff --git a/library/goptions.mli b/library/goptions.mli
index d3e0ac1a6..1a89961ac 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -135,6 +135,18 @@ val declare_string_option: string option_sig -> string write_function
(** {6 Special functions supposed to be used only in vernacentries.ml } *)
+type 'a option_state = {
+ opt_sync : bool;
+ opt_name : string;
+ opt_key : option_name;
+ opt_value : 'a;
+}
+
+type option_value =
+ | BoolValue of bool
+ | IntValue of int option
+ | StringValue of string
+
val get_string_table :
option_name ->
< add : string -> unit;