diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-29 09:44:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-29 09:44:58 +0000 |
| commit | fb7851ec9be42e9d3b77c9f7034c3995f68b2ced (patch) | |
| tree | e34c6a91a2ea9be6a1741d54688a8f38810ad3d2 /library/goptions.mli | |
| 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/goptions.mli')
| -rw-r--r-- | library/goptions.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |