From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 library/goptions.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'library/goptions.ml')

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;
-- 
cgit v1.2.3