diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-18 20:30:27 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-18 20:30:27 +0000 |
commit | 9e89bf92ee52004eaf4fc6491c623b9b7db1da2a (patch) | |
tree | 00b8a22e7b319059b14a5be43c0b580a17624a43 /library/goptions.mli | |
parent | 2d3430f3a49d844fdbff5db8d706b372ffec7a17 (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.mli | 12 |
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; |