Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 23 insertions, 22 deletions

diff --git a/library/goptions.mli b/library/goptions.mli
index 78c4d8e6..d25c1202 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -1,16 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: goptions.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** This module manages customization parameters at the vernacular level     *)
 
-(* This module manages customization parameters at the vernacular level     *)
-
-(* Two kinds of things are managed : tables and options value
+(** Two kinds of things are managed : tables and options value
    - Tables are created by applying the [MakeTable] functor.
    - Variables storing options value are created by applying one of the
    [declare_int_option], [declare_bool_option], ... functions.
@@ -40,12 +38,11 @@
 
        Set Tata Tutu Titi.
        Unset Tata Tutu Titi.
-       Print Table Tata Tutu Titi. (* synonym: Test Table Tata Tutu Titi. *)
+       Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *)
 
    The created table/option may be declared synchronous or not
    (synchronous = consistent with the resetting commands)                   *)
 
-(*i*)
 open Pp
 open Util
 open Names
@@ -53,18 +50,12 @@ open Libnames
 open Term
 open Nametab
 open Mod_subst
-(*i*)
-
-(*s Things common to tables and options. *)
-
-(* The type of table/option keys *)
-type option_name = string list
 
-val error_undeclared_key : option_name -> 'a
+type option_name = Goptionstyp.option_name
 
-(*s Tables. *)
+(** {6 Tables. } *)
 
-(* The functor [MakeStringTable] declares a table containing objects
+(** The functor [MakeStringTable] declares a table containing objects
    of type [string]; the function [member_message] say what to print
    when invoking the "Test Toto Titi foo." command; at the end [title]
    is the table name printed when invoking the "Print Toto Titi."
@@ -85,7 +76,7 @@ sig
   val elements : unit -> string list
 end
 
-(* The functor [MakeRefTable] declares a new table of objects of type
+(** The functor [MakeRefTable] declares a new table of objects of type
    [A.t] practically denoted by [reference]; the encoding function
    [encode : reference -> A.t] is typically a globalization function,
    possibly with some restriction checks; the function
@@ -113,21 +104,26 @@ module MakeRefTable :
     end
 
 
-(*s Options. *)
+(** {6 Options. } *)
 
-(* These types and function are for declaring a new option of name [key]
+(** These types and function are for declaring a new option of name [key]
    and access functions [read] and [write]; the parameter [name] is the option name
    used when printing the option value (command "Print Toto Titi." *)
 
 type 'a option_sig = {
   optsync    : bool;
+  (** whether the option is synchronous w.r.t to the section/module system. *)
+  optdepr    : bool;
+  (** whether the option is DEPRECATED *)
   optname    : string;
+  (** a short string describing the option *)
   optkey     : option_name;
+  (** the low-level name of this option *)
   optread    : unit -> 'a;
   optwrite   : 'a -> unit
 }
 
-(* When an option is declared synchronous ([optsync] is [true]), the output is
+(** When an option is declared synchronous ([optsync] is [true]), the output is
    a synchronous write function. Otherwise it is [optwrite] *)
 
 type 'a write_function = 'a -> unit
@@ -137,7 +133,9 @@ val declare_bool_option  : bool option_sig   -> bool write_function
 val declare_string_option: string option_sig -> string write_function
 
 
-(*s Special functions supposed to be used only in vernacentries.ml *)
+(** {6 Special functions supposed to be used only in vernacentries.ml } *)
+
+module OptionMap : Map.S with type key = option_name
 
 val get_string_table :
   option_name ->
@@ -153,7 +151,8 @@ val get_ref_table :
       mem : reference -> unit;
       print : unit >
 
-(* The first argument is a locality flag. [Some true] = "Local", [Some false]="Global". *)
+(** The first argument is a locality flag.
+    [Some true] = "Local", [Some false]="Global". *)
 val set_int_option_value_gen    : bool option -> option_name -> int option -> unit
 val set_bool_option_value_gen   : bool option -> option_name -> bool   -> unit
 val set_string_option_value_gen : bool option -> option_name -> string -> unit
@@ -165,5 +164,7 @@ val set_string_option_value : option_name -> string -> unit
 
 val print_option_value : option_name -> unit
 
+val get_tables : unit -> Goptionstyp.option_state OptionMap.t
 val print_tables : unit -> unit
 
+val error_undeclared_key : option_name -> 'a