Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 4 insertions, 2 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 4d36e1c5..a9b33235 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: goptions.ml 9060 2006-07-27 15:30:35Z notin $ *)
+(* $Id: goptions.ml 10348 2007-12-06 17:36:14Z aspiwack $ *)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -25,10 +25,12 @@ open Mod_subst
 type option_name =
   | PrimaryTable of string
   | SecondaryTable of string * string
+  | TertiaryTable of string * string * string
 
 let nickname = function
   | PrimaryTable s         -> s
   | SecondaryTable (s1,s2) -> s1^" "^s2
+  | TertiaryTable (s1,s2,s3) -> s1^" "^s2^" "^s3
 
 let error_undeclared_key key =
   error ((nickname key)^": no table or option of this type")
@@ -206,7 +208,7 @@ module MakeRefTable =
   functor (A : RefConvertArg) -> MakeTable (RefConvert(A))
 
 (****************************************************************************)
-(* 2- Options                                                               *)
+(* 2- Flags.                                                              *)
 
 type 'a option_sig = {
   optsync  : bool;