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.

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
---
 contrib/interface/xlate.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'contrib/interface')

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,
-- 
cgit v1.2.3