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

7 files changed, 50 insertions, 42 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,
diff --git a/doc/refman/Natural.tex b/doc/refman/Natural.tex
index 69dfab87c6..9a9abe5dff 100644
--- a/doc/refman/Natural.tex
+++ b/doc/refman/Natural.tex
@@ -121,7 +121,7 @@ declared as implicit, type
 
 \comindex{Test Natural}
 \begin{coq_example*}
-Test Natural Implicit lem1.
+Test Natural Implicit for lem1.
 \end{coq_example*}
 
 \subsubsection*{Implicit proof constructors}
@@ -211,7 +211,7 @@ By default, the data type \verb=nat= and the inductive connectives
 
 As above, you can remove or test a constant declared implicit.  Use
 {\tt Remove Natural Contractible $id$} or {\tt Test Natural
-Contractible $id$}.
+Contractible for $id$}.
 
 \asubsection{Contractible proof steps}
 
@@ -328,7 +328,7 @@ a non inductive transparent definition.
 As for implicit and contractible definitions, you can remove or test a
 non inductive definition declared transparent.
 Use \texttt{Remove Natural Transparent} \ident or 
-\texttt{Test Natural Transparent} \ident.
+\texttt{Test Natural Transparent for} \ident.
 
 \subsubsection*{Transparent inductive definitions}
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 769927cafa..f6e44f91ab 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -424,7 +424,7 @@ The default is to not print synthesisable types.
 \subsubsection{Printing matching on irrefutable pattern
 \comindex{Add Printing Let {\ident}}
 \comindex{Remove Printing Let {\ident}}
-\comindex{Test Printing Let {\ident}}
+\comindex{Test Printing Let for {\ident}}
 \comindex{Print Table Printing Let}}
 
 If an inductive type has just one constructor,
@@ -443,7 +443,7 @@ pattern-matching is written using a {\tt let} expression.
 This removes {\ident} from this list.
 
 \begin{quote}
-{\tt Test Printing Let {\ident}.}
+{\tt Test Printing Let for {\ident}.}
 \end{quote}
 This tells if {\ident} belongs to the list.
 
@@ -460,7 +460,7 @@ it is sensible to the command {\tt Reset}.
 \subsubsection{Printing matching on booleans
 \comindex{Add Printing If {\ident}}
 \comindex{Remove Printing If {\ident}}
-\comindex{Test Printing If {\ident}}
+\comindex{Test Printing If for {\ident}}
 \comindex{Print Table Printing If}}
 
 If an inductive type is isomorphic to the boolean type,
@@ -479,7 +479,7 @@ pattern-matching is written using an {\tt if} expression.
 This removes {\ident} from this list.
 
 \begin{quote}
-{\tt Test Printing If {\ident}.}
+{\tt Test Printing If for {\ident}.}
 \end{quote}
 This tells if {\ident} belongs to the list.
 
@@ -498,7 +498,7 @@ it is sensible to the command {\tt Reset}.
 This example emphasizes what the printing options offer.
 
 \begin{coq_example}
-Test Printing Let prod.
+Test Printing Let for prod.
 Print fst.
 Remove Printing Let prod.
 Unset Printing Synth.
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
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 6d0e3ffc43..ce9aacee81 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -551,48 +551,41 @@ GEXTEND Gram
 	  VernacAddMLPath (true, dir)
 
       (* Pour intervenir sur les tables de param��tres *)
-      | "Set"; table = IDENT; field = IDENT; v = option_value ->
-  	  VernacSetOption (SecondaryTable (table,field),v)
-      | "Set"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value ->
-  	  VernacAddOption (SecondaryTable (table,field),lv)
-      | "Set"; table = IDENT; field = IDENT ->
-  	  VernacSetOption (SecondaryTable (table,field),BoolValue true)
-      | IDENT "Unset"; table = IDENT; field = IDENT ->
-  	  VernacUnsetOption (SecondaryTable (table,field))
-      | IDENT "Unset"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value ->
-  	  VernacRemoveOption (SecondaryTable (table,field),lv)
-      | "Set"; table = IDENT; value = option_value ->
-  	  VernacSetOption (PrimaryTable table, value)
-      | "Set"; table = IDENT ->
-  	  VernacSetOption (PrimaryTable table, BoolValue true)
-      | IDENT "Unset"; table = IDENT ->
-  	  VernacUnsetOption (PrimaryTable table)
-
-      | IDENT "Print"; IDENT "Table"; table = IDENT; field = IDENT ->
-	  VernacPrintOption (SecondaryTable (table,field))
-      | IDENT "Print"; IDENT "Table"; table = IDENT ->
-	  VernacPrintOption (PrimaryTable table)
+      | "Set"; table = option_table; v = option_value ->
+  	  VernacSetOption (table,v)
+      | "Set"; table = option_table ->
+  	  VernacSetOption (table,BoolValue true)
+      | IDENT "Unset"; table = option_table ->
+  	  VernacUnsetOption table
+
+      | IDENT "Print"; IDENT "Table"; table = option_table ->
+	  VernacPrintOption table
 
       | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
         -> VernacAddOption (SecondaryTable (table,field), v)
-
       (* Un value global ci-dessous va ��tre cach�� par un field au dessus! *)
+      (* Dans la pratique, on a donn�� priorit�� aux tables secondaires *)
       | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value ->
           VernacAddOption (PrimaryTable table, v)
+      | IDENT "Add"; table = IDENT; field = IDENT; field2 = IDENT; 
+	  v = LIST1 option_ref_value
+        -> VernacAddOption (TertiaryTable (table,field,field2), v)
 
-      | IDENT "Test"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
-        -> VernacMemOption (SecondaryTable (table,field), v)
-      | IDENT "Test"; table = IDENT; field = IDENT ->
-          VernacPrintOption (SecondaryTable (table,field))
-      | IDENT "Test"; table = IDENT; v = LIST1 option_ref_value ->
-          VernacMemOption (PrimaryTable table, v)
-      | IDENT "Test"; table = IDENT ->
-          VernacPrintOption (PrimaryTable table)
+      | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value
+        -> VernacMemOption (table, v)
+      | IDENT "Test"; table = option_table ->
+          VernacPrintOption table
 
       | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
         -> VernacRemoveOption (SecondaryTable (table,field), v)
+      (* Un value global ci-dessous va ��tre cach�� par un field au dessus! *)
+      (* Dans la pratique, on a donn�� priorit�� aux tables secondaires *)
       | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
 	  VernacRemoveOption (PrimaryTable table, v) 
+      | IDENT "Remove"; table = IDENT; field = IDENT; field2 = IDENT; 
+	  v = LIST1 option_ref_value ->
+	  VernacRemoveOption (TertiaryTable (table,field,field2), v) 
+
       | IDENT "proof" -> VernacDeclProof
       | "return" -> VernacReturn ]]
   ;
@@ -657,6 +650,11 @@ GEXTEND Gram
     [ [ id = global   -> QualidRefValue id
       | s  = STRING   -> StringRefValue s ] ]
   ;
+  option_table:
+    [ [ f1 = IDENT; f2 = IDENT; f3 = IDENT -> TertiaryTable (f1,f2,f3)
+      | f1 = IDENT; f2 = IDENT -> SecondaryTable (f1,f2)
+      | f1 = IDENT -> PrimaryTable f1 ] ]
+  ;
   as_dirpath:
     [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ]
   ;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 9b01863680..e9d960e37c 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -162,6 +162,9 @@ let pr_option_ref_value = function
 let pr_printoption a b = match a with
   | Goptions.PrimaryTable table -> str table ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b
   | Goptions.SecondaryTable (table,field) -> str table ++ spc() ++ str field ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b
+  | Goptions.TertiaryTable (table,field1,field2) -> str table ++ spc() ++
+      str field1 ++ spc() ++ str field2 ++ 
+      pr_opt (prlist_with_sep sep pr_option_ref_value) b
 
 let pr_set_option a b = 
   let pr_opt_value = function