RĂ©paration des options Set Printing and co

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2052 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 151 insertions, 150 deletions

diff --git a/Makefile b/Makefile
index 5fb3bb2c9..39e61a611 100644
--- a/Makefile
+++ b/Makefile
@@ -82,8 +82,8 @@ KERNEL=kernel/names.cmo kernel/univ.cmo \
        kernel/indtypes.cmo kernel/cooking.cmo kernel/safe_typing.cmo
 
 LIBRARY=library/libobject.cmo library/summary.cmo library/nametab.cmo \
-	library/lib.cmo library/goptions.cmo \
-	library/global.cmo library/opaque.cmo \
+	library/lib.cmo library/global.cmo \
+	library/goptions.cmo library/opaque.cmo \
 	library/library.cmo library/states.cmo \
 	library/impargs.cmo library/indrec.cmo library/declare.cmo 
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 8c0c08cef..94fb12668 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -14,6 +14,7 @@ open Pp
 open Util
 open Libobject
 open Names
+open Term
 
 (****************************************************************************)
 (* 0- Common things                                                         *)
@@ -33,7 +34,7 @@ type value =
   | BoolValue   of bool
   | IntValue    of int
   | StringValue of string
-  | IdentValue  of identifier
+  | IdentValue  of global_reference
 
 (****************************************************************************)
 (* 1- Tables                                                                *)
@@ -167,19 +168,19 @@ let get_ident_table k = List.assoc (nickname k) !ident_table
 module type IdentConvertArg =
 sig
   type t
-  val encode : identifier -> t
+  val encode : global_reference -> t
   val check : t -> unit
   val printer : t -> std_ppcmds
   val key : option_name
   val title : string
-  val member_message : identifier -> bool -> string
+  val member_message : global_reference -> bool -> string
   val synchronous : bool
 end
 
 module IdentConvert = functor (A : IdentConvertArg) -> 
 struct
   type t = A.t
-  type key = identifier
+  type key = global_reference
   let table = ident_table
   let encode = A.encode
   let check = A.check
@@ -207,6 +208,7 @@ module OptionMap = Map.Make(Key)
 let sync_value_tab = ref OptionMap.empty
 let async_value_tab = ref OptionMap.empty
 
+
 (* Tools for synchronous options *)
 
 let load_sync_value _ = ()
@@ -246,7 +248,6 @@ let get_option key =
 
 
 (* 2-a. Declaring synchronous options *)
-
 type 'a sync_option_sig = {
   optsyncname    : string;
   optsynckey     : option_name;
@@ -310,7 +311,6 @@ let declare_async_string_option =
     (fun v -> StringValue v)
     (function StringValue v -> v | _ -> anomaly "async_option")
 
-
 (* 3- User accessible commands *)
 
 (* Setting values of options *)
@@ -349,7 +349,7 @@ let msg_sync_option_value (name,v) =
     | BoolValue false -> [< 'sTR "false" >]
     | IntValue n      -> [< 'iNT n >]
     | StringValue s   -> [< 'sTR s >]
-    | IdentValue id    -> [< pr_id id >]
+    | IdentValue id    -> [< 'sTR (Global.string_of_global id) >]
 
 let msg_async_option_value (name,vref) =
   match vref with
@@ -360,10 +360,14 @@ let msg_async_option_value (name,vref) =
 
 let print_option_value key =
   let (name,info) = get_option key in
-  let s = match info with
-    | Sync v -> msg_sync_option_value (name,v)
-      | Async (read,write) -> msg_sync_option_value (name,read ())
-  in mSG [< 'sTR ("Current value of "^name^" is "); s; 'fNL >]
+  let s = match info with Sync v -> v | Async (read,write) -> read () in
+  match s with
+    | BoolValue b -> 
+	mSG [< 'sTR("The "^name^" mode is "^(if b then "on" else "off"));'fNL>]
+    | _ ->
+	mSG [< 'sTR ("Current value of "^name^" is "); 
+	       msg_sync_option_value (name,s); 'fNL >]
+
 
 let print_tables () =
   mSG
diff --git a/library/goptions.mli b/library/goptions.mli
index 012967561..cece47bf2 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -32,20 +32,20 @@
    following vernacular commands:
 
        Set Tata Tutu val.
-       Print Tata Tutu.
+       Print Table Tata Tutu.
 
    If it is the declaration of a boolean value, the following
    vernacular commands are made available:
 
        Set Tata Tutu.
        Unset Tata Tutu.
-       Print Tata Tutu.
+       Print Table Tata Tutu. (* synonym: Test Table Tata Tutu. *)
 
    For a primary table, say of name [PrimaryTable("Bidule")], the
    vernacular commands look like
 
       Add Bidule foo.
-      Print Bidule foo.
+      Print Table Bidule foo.
       Set Bidule foo.
       ...
 
@@ -55,6 +55,7 @@
 (*i*)
 open Pp
 open Names
+open Term
 (*i*)
 
 (*s Things common to tables and options. *)
@@ -93,11 +94,11 @@ sig
   val elements : unit -> string list
 end
 
-(* The functor [MakeIdentTable] declares a new table of [identifier];
+(* The functor [MakeIdentTable] declares a new table of [global_reference];
    for generality, identifiers may be internally encode in other type
-   which is [A.t] through an encoding function [encode : identifier ->
-   A.t] (typically, [A.t] is the persistent [section_path] associated
-   to the currentdenotation of the [identifier] and the encoding function
+   which is [A.t] through an encoding function [encode : global_reference ->
+   A.t] (typically, [A.t] is the persistent [global_reference] associated
+   to the currentdenotation of the [global_reference] and the encoding function
    is the globalization function); the function [check] is for testing
    if a given object is allowed to be added to the table; the function
    [member_message] say what to print when invoking the "Test Toto
@@ -110,12 +111,12 @@ module MakeIdentTable :
   functor
     (A : sig
            type t
-           val encode : identifier -> t
+           val encode : global_reference -> t
            val check : t -> unit
            val printer : t -> std_ppcmds
            val key : option_name
            val title : string
-           val member_message : identifier -> bool -> string
+           val member_message : global_reference -> bool -> string
            val synchronous : bool
          end) ->
     sig
@@ -169,9 +170,9 @@ val get_string_table :
 
 val get_ident_table :
   option_name ->
-    < add : identifier -> unit;
-      remove : identifier -> unit;
-      mem : identifier -> unit;
+    < add : global_reference -> unit;
+      remove : global_reference -> unit;
+      mem : global_reference -> unit;
       print : unit >
 
 val set_int_option_value    : option_name -> int    -> unit
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index b2b04a2d7..2a447a910 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -185,37 +185,6 @@ GEXTEND Gram
       | IDENT "Unset"; IDENT "Hyps_limit" ->
           <:ast< (UNSETHYPSLIMIT) >>
 
-      (* Standardized syntax for Implicit Arguments *)
-      | "Set"; IDENT "Implicit"; IDENT "Arguments" ->
-          <:ast< (IMPLICIT_ARGS_ON) >>
-      | IDENT "Unset"; IDENT "Implicit"; IDENT "Arguments" ->
-          <:ast< (IMPLICIT_ARGS_OFF) >>
-      | IDENT "Test"; IDENT "Implicit"; IDENT "Arguments" ->
-          <:ast< (TEST_IMPLICIT_ARGS) >>
-
-      (* Set printing depth *)
-      (* An explicit entry, to be factorized with Printing Coercions *)
-      | "Set"; table = IDENT "Printing"; field = IDENT "Depth"; n = numarg ->
-          <:ast< (SetTableField ($VAR $table) ($VAR $field) $n) >>
-
-      (* Set printing of coercions *)
-      | "Set"; IDENT "Printing"; IDENT "Coercion"; 
-	qidl = ne_qualidarg_list ->
-	  <:ast< (PRINTING_COERCIONS_ON ($LIST $qidl)) >>
-      | "Set"; IDENT "Printing"; IDENT "Coercions" ->
-          <:ast< (PRINTING_COERCIONS_ON) >>
-      | IDENT "Unset"; IDENT "Printing"; IDENT "Coercion"; 
-	qidl = ne_qualidarg_list ->
-          <:ast< (PRINTING_COERCIONS_OFF ($LIST $qidl)) >>
-      | IDENT "Unset"; IDENT "Printing"; IDENT "Coercions" ->
-          <:ast< (PRINTING_COERCIONS_OFF) >>
-      | IDENT "Test"; IDENT "Printing"; IDENT "Coercion";
-	qidl = ne_qualidarg_list ->
-          <:ast< (TEST_PRINTING_COERCIONS ($LIST $qidl)) >>
-      | IDENT "Test"; IDENT "Printing"; IDENT "Coercions" ->
-          <:ast< (TEST_PRINTING_COERCIONS) >>
-
-
       (* Pour intervenir sur les tables de paramètres *)
       | "Set"; table = identarg; field = identarg;
                       value = option_value ->
@@ -224,6 +193,8 @@ GEXTEND Gram
           <:ast< (SetTableField $table $field) >>
       | IDENT "Unset"; table = identarg; field = identarg ->
           <:ast< (UnsetTableField $table $field) >>
+      | IDENT "Unset"; table = identarg; field = identarg; id = qualidarg ->
+          <:ast< (RemoveTableField $table $field $id) >>
       | "Set"; table = identarg; value = option_value ->
           <:ast< (SetTableField $table $value) >>
       | "Set"; table = identarg ->
@@ -236,33 +207,37 @@ GEXTEND Gram
       (* Le cas suivant inclut aussi le "Print id" standard *)
       | IDENT "Print"; IDENT "Table"; table = identarg ->
           <:ast< (PrintOption $table) >>
-      | IDENT "Add"; table = identarg; field = identarg; id = identarg
+      | IDENT "Add"; table = identarg; field = identarg; id = qualidarg
         -> <:ast< (AddTableField $table $field $id) >>
       | IDENT "Add"; table = identarg; field = identarg; id = stringarg
         -> <:ast< (AddTableField $table $field $id) >>
-      | IDENT "Add"; table = identarg; id = identarg
+      | IDENT "Add"; table = identarg; id = qualidarg
         -> <:ast< (AddTableField $table $id) >>
       | IDENT "Add"; table = identarg; id = stringarg
         -> <:ast< (AddTableField $table $id) >>
-      | IDENT "Test"; table = identarg; field = identarg; id = identarg
+      | IDENT "Test"; table = identarg; field = identarg; id = qualidarg
         -> <:ast< (MemTableField $table $field $id) >>
       | IDENT "Test"; table = identarg; field = identarg; id = stringarg
         -> <:ast< (MemTableField $table $field $id) >>
       | IDENT "Test"; table = identarg; id = identarg
         -> <:ast< (MemTableField $table $id) >>
+      | IDENT "Test"; table = identarg; id = qualidarg
+        -> <:ast< (MemTableField $table $id) >>
       | IDENT "Test"; table = identarg; id = stringarg
         -> <:ast< (MemTableField $table $id) >>
-      | IDENT "Remove"; table = identarg; field = identarg; id = identarg ->
+      | IDENT "Test"; table = identarg
+        -> <:ast< (MemTableField $table) >>
+      | IDENT "Remove"; table = identarg; field = identarg; id = qualidarg ->
           <:ast< (RemoveTableField $table $field $id) >>
       | IDENT "Remove"; table = identarg; field = identarg; id = stringarg ->
           <:ast< (RemoveTableField $table $field $id) >>
-      | IDENT "Remove"; table = identarg; id = identarg ->
+      | IDENT "Remove"; table = identarg; id = qualidarg ->
           <:ast< (RemoveTableField $table $id) >>
       | IDENT "Remove"; table = identarg; id = stringarg ->
           <:ast< (RemoveTableField $table $id) >> ] ]
   ;
   option_value:
-    [ [ id = identarg    -> id
+    [ [ id = qualidarg    -> id
       | n  = numarg      -> n
       | s  = stringarg   -> s ] ]
   ;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1af83f722..a3d6d86cf 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -98,15 +98,12 @@ let used_of = global_vars_and_consts
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
 
-let encode_inductive id =
+let encode_inductive ref =
   let (indsp,_ as ind) =
-    try 
-      match kind_of_term (global_reference CCI id) with
+      match kind_of_term (constr_of_reference Evd.empty (Global.env()) ref)with
         | IsMutInd (indsp,args) -> (indsp,args)
 	| _ -> errorlabstrm "indsp_of_id" 
-	    [< 'sTR ((string_of_id id)^" is not an inductive type") >]
-    with Not_found -> 
-      error ("Cannot find reference "^(string_of_id id))
+	    [< 'sTR ((Global.string_of_global ref)^" is not an inductive type") >]
   in
   let mis = Global.lookup_mind_specif ind in
   let constr_lengths = Array.map List.length (mis_recarg mis) in
@@ -134,7 +131,7 @@ module PrintingCasesMake =
   functor (Test : sig 
      val test : int array -> bool
      val error_message : string
-     val member_message : identifier -> bool -> string
+     val member_message : global_reference -> bool -> string
      val field : string
      val title : string
   end) ->
@@ -159,10 +156,10 @@ module PrintingCasesIf =
     let title = "Types leading to pretty-printing of Cases using a `if' form: "
     let member_message id = function
       | true  -> 
-          "Cases on elements of " ^ (string_of_id id)
+          "Cases on elements of " ^ (Global.string_of_global id)
           ^ " are printed using a `if' form"
       | false -> 
-          "Cases on elements of " ^ (string_of_id id)
+          "Cases on elements of " ^ (Global.string_of_global id)
           ^ " are not printed using `if' form"
   end)
 
@@ -175,10 +172,10 @@ module PrintingCasesLet =
       "Types leading to a pretty-printing of Cases using a `let' form:"
     let member_message id = function
       | true  -> 
-          "Cases on elements of " ^ (string_of_id id)
+          "Cases on elements of " ^ (Global.string_of_global id)
           ^ " are printed using a `let' form"
       | false -> 
-          "Cases on elements of " ^ (string_of_id id)
+          "Cases on elements of " ^ (Global.string_of_global id)
           ^ " are not printed using a `let' form"
   end)
 
@@ -199,7 +196,7 @@ let force_wildcard () = !wildcard_value
 
 let _ =                           
   declare_async_bool_option 
-    { optasyncname  = "the forced wildcard option";
+    { optasyncname  = "forced wildcard";
       optasynckey   = SecondaryTable ("Printing","Wildcard");
       optasyncread  = force_wildcard;
       optasyncwrite = (fun v -> wildcard_value := v) }
@@ -209,7 +206,7 @@ let synthetize_type () = !synth_type_value
 
 let _ = 
   declare_async_bool_option 
-    { optasyncname = "the synthesisablity";
+    { optasyncname = "synthesizability";
       optasynckey   = SecondaryTable ("Printing","Synth");
       optasyncread = synthetize_type;
       optasyncwrite = (fun v -> synth_type_value := v) }
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 201896d90..bdf448afe 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -484,6 +484,12 @@ let _ =
 	      make_focus 0; reset_top_of_tree (); show_open_subgoals ())
        | _  -> bad_vernac_args "UNFOCUS")
 
+let _ = declare_async_bool_option 
+	  {optasyncname  = "implicit arguments";
+	   optasynckey   = (SecondaryTable ("Implicit","Arguments"));
+	   optasyncread  = Impargs.is_implicit_args;
+	   optasyncwrite = Impargs.make_implicit_args }
+
 let _ =          
   add "IMPLICIT_ARGS_ON"
     (function 
@@ -515,69 +521,12 @@ let coercion_of_qualid loc qid =
       [< Printer.pr_global ref; 'sTR" is not a coercion" >];
   coe
 
-let _ =
-  add "PRINTING_COERCIONS_ON"
-    (function 
-       | [] -> (fun () -> Termast.print_coercions := true)
-       | l ->
-	   let ql =
-	     List.map 
-	       (function
-		  | VARG_QUALID qid -> qid
-		  | _ ->  bad_vernac_args "PRINTING_COERCIONS_ON") l in
-	   (fun () ->
-	      List.iter
-		(fun qid ->
-		   Classops.set_coercion_visibility true
-		     (coercion_of_qualid dummy_loc qid))
-		ql))
-
-let _ =
-  add "PRINTING_COERCIONS_OFF"
-    (function 
-       | [] -> (fun () -> Termast.print_coercions := false)
-       | l -> 
-	   let ql =
-	     List.map 
-	       (function
-		  | VARG_QUALID qid -> qid
-		  | _ ->  bad_vernac_args "PRINTING_COERCIONS_OFF") l in
-	   (fun () ->
-	      List.iter
-		(fun qid ->
-		   Classops.set_coercion_visibility false 
-		     (coercion_of_qualid dummy_loc qid))
-		ql))
+let _ = declare_async_bool_option 
+	  {optasyncname  = "coercion printing";
+	   optasynckey   = (SecondaryTable ("Printing","Coercions"));
+	   optasyncread  = (fun () -> !Termast.print_coercions);
+	   optasyncwrite = (fun b ->  Termast.print_coercions := b) }
 
-let _ =
-  add "TEST_PRINTING_COERCIONS"
-    (function 
-       | [] ->
-           (fun () ->
-              if !(Termast.print_coercions) = true then
-		message "Printing of coercions is set"
-              else 
-		message "Printing of coercions is unset")
-       | l -> 
-	   let ql =
-	     List.map 
-	       (function
-		  | VARG_QUALID qid -> qid
-		  | _  -> bad_vernac_args "TEST_PRINTING_COERCIONS") l in
-	   (fun () ->
-              List.iter
-		(fun qid ->
-		   let coe = coercion_of_qualid dummy_loc qid in
-	           if Classops.is_coercion_visible coe then
-		     message
-		       ("Printing of coercion "^(Nametab.string_of_qualid qid)^
-			" is set")
-		   else 
-		     message 
-		       ("Printing of coercion "^(Nametab.string_of_qualid qid)^
-			" is unset"))
-		ql))
-    
 let number_list = 
   List.map (function VARG_NUMBER n -> n | _ -> bad_vernac_args "Number list") 
 
@@ -838,7 +787,7 @@ let _ =
        | _ -> bad_vernac_args "PrintSec")
 
 let _ = declare_async_bool_option 
-	  {optasyncname  = "Silent";
+	  {optasyncname  = "silent";
 	   optasynckey   = (PrimaryTable "Silent");
 	   optasyncread  = is_silent;
 	   optasyncwrite = make_silent }
@@ -1498,6 +1447,20 @@ let _ =
 let _ =
   add "SetTableField"
     (function
+       (* Hook for Printing Coercions *)
+       | (VARG_IDENTIFIER t) :: (VARG_IDENTIFIER f) :: l 
+	 when t = id_of_string "Printing" && f = id_of_string "Coercion" -> 
+	   let ql =
+	     List.map 
+	       (function
+		  | VARG_QUALID qid -> qid
+		  | _ ->  bad_vernac_args "PRINTING_COERCIONS_ON") l in
+	   (fun () ->
+	      List.iter
+		(fun qid ->
+		   Classops.set_coercion_visibility true
+		     (coercion_of_qualid dummy_loc qid))
+		ql)
        | [(VARG_IDENTIFIER t);(VARG_IDENTIFIER f);arg] -> 
 	   (fun () ->
 	      let key = 
@@ -1541,12 +1504,12 @@ let _ =
 let _ =
   add "AddTableField"
     (function
-       | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_IDENTIFIER v] -> 
+       | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_QUALID v] -> 
 	   (fun () ->
 	      let key = 
 		SecondaryTable (string_of_id t,string_of_id f) in
 	      try 
-		(get_ident_table key)#add v
+		(get_ident_table key)#add (locate_qualid dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING s] -> 
@@ -1557,11 +1520,11 @@ let _ =
 		(get_string_table key)#add s
 	      with Not_found -> 
 		error_undeclared_key key)
-       | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] ->
+       | [VARG_IDENTIFIER t; VARG_QUALID v] ->
 	   (fun () ->
 	      let key = PrimaryTable (string_of_id t) in
 	      try 
-		(get_ident_table key)#add v
+		(get_ident_table key)#add (locate_qualid dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_STRING s] ->
@@ -1576,12 +1539,26 @@ let _ =
 let _ =
   add "RemoveTableField"
     (function
-       | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_IDENTIFIER v] -> 
+       (* Hook for Printing Coercions *)
+       | (VARG_IDENTIFIER t) :: (VARG_IDENTIFIER f) :: l 
+	 when t = id_of_string "Printing" && f = id_of_string "Coercion" -> 
+	   let ql =
+	     List.map 
+	       (function
+		  | VARG_QUALID qid -> qid
+		  | _ ->  bad_vernac_args "PRINTING_COERCIONS_OFF") l in
+	   (fun () ->
+	      List.iter
+		(fun qid ->
+		   Classops.set_coercion_visibility false 
+		     (coercion_of_qualid dummy_loc qid))
+		ql)
+       | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_QUALID v] -> 
 	   (fun () ->
 	      let key = 
 		SecondaryTable (string_of_id t,string_of_id f) in
 	      try 
-		(get_ident_table key)#remove v
+		(get_ident_table key)#remove (locate_qualid dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> 
@@ -1592,11 +1569,11 @@ let _ =
 		(get_string_table key)#remove v
 	      with Not_found -> 
 		error_undeclared_key key)
-       | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> 
+       | [VARG_IDENTIFIER t; VARG_QUALID v] -> 
 	   (fun () ->
 	      let key = PrimaryTable (string_of_id t) in
 	      try 
-		(get_ident_table key)#remove v
+		(get_ident_table key)#remove (locate_qualid dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_STRING v] -> 
@@ -1611,12 +1588,33 @@ let _ =
 let _ =
   add "MemTableField"
     (function
-       | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_IDENTIFIER v] -> 
+       (* Hook for Printing Coercions *)
+       | (VARG_IDENTIFIER t) :: (VARG_IDENTIFIER f) :: l 
+	 when t = id_of_string "Printing" && f = id_of_string "Coercion" -> 
+	   let ql =
+	     List.map 
+	       (function
+		  | VARG_QUALID qid -> qid
+		  | _  -> bad_vernac_args "TEST_PRINTING_COERCIONS") l in
+	   (fun () ->
+              List.iter
+		(fun qid ->
+		   let coe = coercion_of_qualid dummy_loc qid in
+	           if Classops.is_coercion_visible coe then
+		     message
+		       ("Printing of coercion "^(Nametab.string_of_qualid qid)^
+			" is set")
+		   else 
+		     message 
+		       ("Printing of coercion "^(Nametab.string_of_qualid qid)^
+			" is unset"))
+		ql)
+       | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_QUALID v] -> 
 	   (fun () ->
 	      let key = 
 		SecondaryTable (string_of_id t,string_of_id f) in
 	      try 
-		(get_ident_table key)#mem v
+		(get_ident_table key)#mem (locate_qualid dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> 
@@ -1627,13 +1625,26 @@ let _ =
 		(get_string_table key)#mem v
 	      with Not_found -> 
 		error_undeclared_key key)
-       | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> 
+       | [VARG_IDENTIFIER t; VARG_QUALID v] ->
 	   (fun () ->
 	      let key = PrimaryTable (string_of_id t) in
 	      try 
-		(get_ident_table key)#mem v
+		(get_ident_table key)#mem (locate_qualid dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
+       | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> 
+	   (fun () ->
+	      let key = SecondaryTable (string_of_id t, string_of_id v) in
+	    try 
+	      (get_ident_table key)#print
+	    with not_found ->
+	    try 
+	      (get_string_table key)#print
+	    with not_found ->
+            try 
+	      print_option_value key
+            with Not_found -> 
+	      error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_STRING v] -> 
 	   (fun () ->
 	      let key = PrimaryTable (string_of_id t) in
@@ -1641,6 +1652,19 @@ let _ =
 		(get_string_table key)#mem v
 	      with Not_found -> 
 		error_undeclared_key key)
+       | [VARG_IDENTIFIER t] -> 
+	 (fun () ->
+	    let key = PrimaryTable (string_of_id t) in
+	    try 
+	      (get_ident_table key)#print
+	    with not_found ->
+	    try 
+	      (get_string_table key)#print
+	    with not_found ->
+            try 
+	      print_option_value key
+            with Not_found -> 
+		error_undeclared_key key)
        |  _ -> bad_vernac_args "TableField")
 
 let _ =