diff options
| author | herbelin | 2007-04-29 09:44:58 +0000 |
|---|---|---|
| committer | herbelin | 2007-04-29 09:44:58 +0000 |
| commit | fb7851ec9be42e9d3b77c9f7034c3995f68b2ced (patch) | |
| tree | e34c6a91a2ea9be6a1741d54688a8f38810ad3d2 /library | |
| parent | 42147c4437754601b7a420facc3b0bdf1ea5ea6e (diff) | |
Ajout possibilité d'options à trois mots.
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
Diffstat (limited to 'library')
| -rw-r--r-- | library/goptions.ml | 2 | ||||
| -rw-r--r-- | library/goptions.mli | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 4eb8f2402a..4be15569e9 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") diff --git a/library/goptions.mli b/library/goptions.mli index 4709fc1c84..53f6a6cdb2 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 |