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 /contrib/interface | |
| 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 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 110ba8243b..0101b10967 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -2102,13 +2102,15 @@ let rec xlate_vernac = let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in CT_set_option(table1) | VernacSetOption (table, v) -> let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in let value = match v with | BoolValue _ -> assert false @@ -2121,7 +2123,8 @@ let rec xlate_vernac = let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in CT_unset_option(table1) | VernacAddOption (table, l) -> let values = @@ -2136,7 +2139,8 @@ let rec xlate_vernac = let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in CT_set_option_value2(table1, CT_id_or_string_ne_list(fst, values1)) | VernacImport(true, a::l) -> CT_export_id(CT_id_ne_list(reference_to_ct_ID a, |