From fb7851ec9be42e9d3b77c9f7034c3995f68b2ced Mon Sep 17 00:00:00 2001 From: herbelin 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.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'library/goptions.ml') diff --git a/library/goptions.ml b/library/goptions.ml index 4eb8f2402..4be15569e 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -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") -- cgit v1.2.3