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.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'library/goptions.mli')

diff --git a/library/goptions.mli b/library/goptions.mli
index 16744ec4..e076a396 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: goptions.mli 6304 2004-11-16 15:49:08Z sacerdot $ i*)
+(*i $Id: goptions.mli 9810 2007-04-29 09:44:58Z herbelin $ i*)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -68,6 +68,7 @@ open Mod_subst
 type option_name =
   | PrimaryTable of string
   | SecondaryTable of string * string
+  | TertiaryTable of string * string * string
 
 val error_undeclared_key : option_name -> 'a
 
-- 
cgit v1.2.3