From fb7851ec9be42e9d3b77c9f7034c3995f68b2ced Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 29 Apr 2007 09:44:58 +0000
Subject: Ajout possibilité d'options à trois mots.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Suppression au passage syntaxe "Set table field ref", synonyme de "Add
table field ref" et de "Unset table field ref", synonyme de "Remove
table field ref".  Changement de la syntaxe "Test tabel field val" en
""Test tabel field for val".


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9810 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/goptions.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'library/goptions.mli')

diff --git a/library/goptions.mli b/library/goptions.mli
index 4709fc1c8..53f6a6cdb 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -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