Generalized the possibility to refer to a global name by a notation

string in most commands expecting a global name (e.g. 'Print "+"' for
an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation,
possibly surrounded by a scope delimiter). Support for such smart
globals in VERNAC EXTEND to do.

Added a file smartlocate.ml for high-level globalization functions.

Mini-nettoyage metasyntax.ml.



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

8 files changed, 91 insertions, 64 deletions

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 0e91fddbdc..168e532a81 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -37,7 +37,7 @@ GEXTEND Gram
   GLOBAL: 
     bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath
-    ne_string string pattern_ident pattern_identref;
+    ne_string string pattern_ident pattern_identref by_notation smart_global;
   preident:
     [ [ s = IDENT -> s ] ]
   ;
@@ -84,6 +84,13 @@ GEXTEND Gram
       | id = ident -> Ident (loc,id)
       ] ]
   ;
+  by_notation:
+    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (loc,s,sc) ] ]
+  ;
+  smart_global:
+    [ [ c = reference -> Genarg.AN c
+      | ntn = by_notation -> Genarg.ByNotation ntn ] ]
+  ;
   qualid:
     [ [ qid = basequalid -> loc, qid ] ]
   ;
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 875b9dc07c..846246ed06 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -215,11 +215,6 @@ GEXTEND Gram
       | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
           (Some (occs,c1), c2) ] ]
   ;
-  smart_global:
-    [ [ c = global -> AN c
-      | s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> 
-	  ByNotation (loc,s,sc) ] ]
-  ;
   occs_nums:
     [ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl
       | "-"; n = nat_or_var; nl = LIST0 int_or_var ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 9940a13784..272737cc68 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -306,11 +306,11 @@ GEXTEND Gram
       | id = identref; ":="; kind = scheme_kind -> (Some id,kind) ] ]
   ;
   scheme_kind:
-    [ [ IDENT "Induction"; "for"; ind = global;
+    [ [ IDENT "Induction"; "for"; ind = smart_global;
           IDENT "Sort"; s = sort-> InductionScheme(true,ind,s)
-      | IDENT "Minimality"; "for"; ind = global;
+      | IDENT "Minimality"; "for"; ind = smart_global;
           IDENT "Sort"; s = sort-> InductionScheme(false,ind,s)
-      | IDENT "Equality"; "for" ; ind = global -> EqualityScheme(ind)  ] ]
+      | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ]
   ;
   (* Various Binders *)
 (*
@@ -465,17 +465,20 @@ GEXTEND Gram
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
-        IDENT "Transparent"; l = LIST1 global ->
+        IDENT "Transparent"; l = LIST1 smart_global ->
           VernacSetOpacity (use_non_locality (),[Conv_oracle.transparent,l])
-      | IDENT "Opaque"; l = LIST1 global ->
+      | IDENT "Opaque"; l = LIST1 smart_global ->
           VernacSetOpacity (use_non_locality (),[Conv_oracle.Opaque, l])
       | IDENT "Strategy"; l =
-          LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] ->
+          LIST1 [ lev=strategy_level; "["; q=LIST1 smart_global; "]" -> (lev,q)] ->
             VernacSetOpacity (use_locality (),l)
       (* Canonical structure *)
       | IDENT "Canonical"; IDENT "Structure"; qid = global ->
-	  VernacCanonical qid
-      | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
+	  VernacCanonical (AN qid)
+      | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation ->
+	  VernacCanonical (ByNotation ntn)
+      | IDENT "Canonical"; IDENT "Structure"; qid = global;
+          d = def_body ->
           let s = coerce_reference_to_id qid in
 	  VernacDefinition 
 	    ((Global,false,CanonicalStructure),(dummy_loc,s),d,
@@ -496,10 +499,16 @@ GEXTEND Gram
 	   VernacIdentityCoercion (use_locality_exp (), f, s, t)
       | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
 	 s = class_rawexpr; ">->"; t = class_rawexpr -> 
-	  VernacCoercion (enforce_locality_exp (), qid, s, t)
+	  VernacCoercion (enforce_locality_exp (), AN qid, s, t)
+      | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":";
+	 s = class_rawexpr; ">->"; t = class_rawexpr -> 
+	  VernacCoercion (enforce_locality_exp (), ByNotation ntn, s, t)
       | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
-	  VernacCoercion (use_locality_exp (), qid, s, t)
+	  VernacCoercion (use_locality_exp (), AN qid, s, t)
+      | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->";
+         t = class_rawexpr ->
+	  VernacCoercion (use_locality_exp (), ByNotation ntn, s, t)
 	     
       | IDENT "Context"; c = binders_let -> 
 	  VernacContext c
@@ -530,7 +539,7 @@ GEXTEND Gram
       | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
 
       (* Implicit *)
-      | IDENT "Implicit"; IDENT "Arguments"; qid = global; 
+      | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; 
 	   pos = OPT [ "["; l = LIST0 implicit_name; "]" -> 
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
 	   VernacDeclareImplicits (use_section_locality (),qid,pos)
@@ -601,13 +610,13 @@ GEXTEND Gram
 
       (* Printing (careful factorization of entries) *)
       | IDENT "Print"; p = printable -> VernacPrint p
-      | IDENT "Print"; qid = global -> VernacPrint (PrintName qid)
+      | IDENT "Print"; qid = smart_global -> VernacPrint (PrintName qid)
       | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> 
 	  VernacPrint (PrintModuleType qid)
       | IDENT "Print"; IDENT "Module"; qid = global -> 
 	  VernacPrint (PrintModule qid)
       | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n)
-      | IDENT "About"; qid = global -> VernacPrint (PrintAbout qid)
+      | IDENT "About"; qid = smart_global -> VernacPrint (PrintAbout qid)
 
       (* Searching the environment *)
       | IDENT "Search"; c = constr_pattern; l = in_or_out_modules -> 
@@ -674,7 +683,7 @@ GEXTEND Gram
 	  fun g -> VernacCheckMayEval (None, g, c) ] ]
   ;
   printable:
-    [ [ IDENT "Term"; qid = global -> PrintName qid
+    [ [ IDENT "Term"; qid = smart_global -> PrintName qid
       | IDENT "All" -> PrintFullContext
       | IDENT "Section"; s = global -> PrintSectionContext s
       | IDENT "Grammar"; ent = IDENT ->
@@ -690,40 +699,36 @@ GEXTEND Gram
       | IDENT "Graph" -> PrintGraph
       | IDENT "Classes" ->  PrintClasses
       | IDENT "TypeClasses" -> PrintTypeClasses
-      | IDENT "Instances"; qid = global -> PrintInstances qid
+      | IDENT "Instances"; qid = smart_global -> PrintInstances qid
       | IDENT "Ltac"; qid = global -> PrintLtac qid
       | IDENT "Coercions" -> PrintCoercions
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> PrintCoercionPaths (s,t)
       | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions
       | IDENT "Tables" -> PrintTables
-(* Obsolete: was used for cooking V6.3 recipes ??
-      | IDENT "Proof"; qid = global -> PrintOpaqueName qid
-*)
       | IDENT "Hint" -> PrintHintGoal
-      | IDENT "Hint"; qid = global -> PrintHint qid
+      | IDENT "Hint"; qid = smart_global -> PrintHint qid
       | IDENT "Hint"; "*" -> PrintHintDb
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
       | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
-      | IDENT "Implicit"; qid = global -> PrintImplicit qid
+      | IDENT "Implicit"; qid = smart_global -> PrintImplicit qid
       | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt
-      | IDENT "Assumptions"; qid = global -> PrintAssumptions (false, qid)
-      | IDENT "Opaque"; IDENT "Dependencies"; qid = global -> PrintAssumptions (true, qid) ] ]
+      | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, qid)
+      | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, qid) ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
       | IDENT "Sortclass" -> SortClass
-      | qid = global -> RefClass qid ] ]
+      | qid = smart_global -> RefClass qid ] ]
   ;
   locatable:
-    [ [ qid = global -> LocateTerm qid
+    [ [ qid = smart_global -> LocateTerm qid
       | IDENT "File"; f = ne_string -> LocateFile f
       | IDENT "Library"; qid = global -> LocateLibrary qid
-      | IDENT "Module"; qid = global -> LocateModule qid
-      | s = ne_string -> LocateNotation s ] ]
+      | IDENT "Module"; qid = global -> LocateModule qid ] ]
   ;
   option_value:
     [ [ n  = integer   -> IntValue n
@@ -805,7 +810,7 @@ GEXTEND Gram
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; 
        refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
 
-     | IDENT "Arguments"; IDENT "Scope"; qid = global;
+     | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
        "["; scl = LIST0 opt_scope; "]" -> 
 	 VernacArgumentsScope (use_non_locality (),qid,scl)
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 1c9e1e46bf..6b5d03d912 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -273,6 +273,8 @@ module Prim =
     let bigint = Gram.Entry.create "Prim.bigint"
     let string = gec_gen rawwit_string "string"
     let reference = make_gen_entry uprim rawwit_ref "reference"
+    let by_notation = Gram.Entry.create "by_notation"
+    let smart_global = Gram.Entry.create "smart_global"
 
     (* parsed like ident but interpreted as a term *)
     let var = gec_gen rawwit_var "var"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f356ae07e3..cfd05f4f7e 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -182,6 +182,8 @@ module Prim :
     val qualid : qualid located Gram.Entry.e
     val fullyqualid : identifier list located Gram.Entry.e
     val reference : reference Gram.Entry.e
+    val by_notation : (loc * string * string option) Gram.Entry.e
+    val smart_global : reference or_by_notation Gram.Entry.e
     val dirpath : dir_path Gram.Entry.e
     val ne_string : string Gram.Entry.e
     val var : identifier located Gram.Entry.e
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 656c384973..26fa535506 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -50,6 +50,8 @@ let pr_lname = function
     (loc,Name id) -> pr_lident (loc,id)
   | lna -> pr_located pr_name lna
 
+let pr_smart_global = pr_or_by_notation pr_reference
+
 let pr_ltac_id = Libnames.pr_reference
 
 let pr_module = Libnames.pr_reference
@@ -164,7 +166,7 @@ let pr_explanation (e,b,f) =
 let pr_class_rawexpr = function
   | FunClass -> str"Funclass"
   | SortClass -> str"Sortclass"
-  | RefClass qid -> pr_reference qid
+  | RefClass qid -> pr_smart_global qid
 
 let pr_option_ref_value = function
   | QualidRefValue id -> pr_reference id
@@ -304,7 +306,7 @@ let pr_onescheme (idop,schem) =
       | None -> spc ()
     ) ++
     hov 0 ((if dep then str"Induction for" else str"Minimality for")
-    ++ spc() ++ pr_reference ind) ++ spc() ++ 
+    ++ spc() ++ pr_smart_global ind) ++ spc() ++ 
     hov 0 (str"Sort" ++ spc() ++ pr_rawsort s)
   | EqualityScheme ind -> 
     (match idop with
@@ -312,7 +314,7 @@ let pr_onescheme (idop,schem) =
       | None -> spc()
     ) ++
     hov 0 (str"Equality for")
-    ++ spc() ++ pr_reference ind
+    ++ spc() ++ pr_smart_global ind
 
 let begin_of_inductive = function
     [] -> 0
@@ -321,7 +323,7 @@ let begin_of_inductive = function
 let pr_class_rawexpr = function
   | FunClass -> str"Funclass"
   | SortClass -> str"Sortclass"
-  | RefClass qid -> pr_reference qid
+  | RefClass qid -> pr_smart_global qid
 
 let pr_assumption_token many = function
   | (Local,Logical) ->
@@ -508,7 +510,8 @@ let rec pr_vernac = function
   | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function 
       |	None -> str"_"
       |	Some sc -> str sc in 
-    str"Arguments Scope" ++ spc() ++ pr_non_locality local ++ pr_reference q 
+    str"Arguments Scope" ++ spc() ++ pr_non_locality local ++ 
+    pr_smart_global q 
     ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
   | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *)
       hov 0 (hov 0 (str"Infix " ++ pr_locality local
@@ -541,7 +544,7 @@ let rec pr_vernac = function
         | None -> mt()
         | Some r ->
             str"Eval" ++ spc() ++
-            pr_red_expr (pr_constr, pr_lconstr, pr_or_by_notation pr_reference) r ++
+            pr_red_expr (pr_constr, pr_lconstr, pr_smart_global) r ++
             str" in" ++ spc() in
       let pr_def_body = function
         | DefineBody (bl,red,body,d) ->
@@ -690,12 +693,12 @@ let rec pr_vernac = function
   | VernacImport (f,l) ->
       (if f then str"Export" else str"Import") ++ spc() ++
       prlist_with_sep sep pr_import_module l
-  | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_reference q
+  | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q
   | VernacCoercion (s,id,c1,c2) ->
       hov 1 (
 	str"Coercion" ++ (match s with | Local -> spc() ++
 	  str"Local" ++ spc() | Global -> spc()) ++
-	pr_reference id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
+	pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
 	spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
   | VernacIdentityCoercion (s,id,c1,c2) ->
       hov 1 (
@@ -831,10 +834,10 @@ let rec pr_vernac = function
 	 prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
   | VernacDeclareImplicits (local,q,None) ->
-      hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
+      hov 2 (str"Implicit Arguments" ++ spc() ++ pr_smart_global q)
   | VernacDeclareImplicits (local,q,Some imps) ->
       hov 1 (str"Implicit Arguments " ++ pr_non_locality local ++
-	spc() ++ pr_reference q ++ spc() ++
+	spc() ++ pr_smart_global q ++ spc() ++
 	str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
   | VernacReserve (idl,c) ->
       hov 1 (str"Implicit Type" ++
@@ -843,10 +846,10 @@ let rec pr_vernac = function
         pr_lconstr c)
   | VernacSetOpacity(b,[k,l]) when k=Conv_oracle.transparent ->
       hov 1 (str"Transparent" ++ pr_non_locality b ++
-             spc() ++ prlist_with_sep sep pr_reference l)
+             spc() ++ prlist_with_sep sep pr_smart_global l)
   | VernacSetOpacity(b,[Conv_oracle.Opaque,l]) ->
       hov 1 (str"Opaque" ++ pr_non_locality b ++
-             spc() ++ prlist_with_sep sep pr_reference l)
+             spc() ++ prlist_with_sep sep pr_smart_global l)
   | VernacSetOpacity (local,l) ->
       let pr_lev = function
           Conv_oracle.Opaque -> str"opaque"
@@ -855,7 +858,7 @@ let rec pr_vernac = function
         | Conv_oracle.Level n -> int n in
       let pr_line (l,q) =
         hov 2 (pr_lev l ++ spc() ++
-               str"[" ++ prlist_with_sep sep pr_reference q ++ str"]") in
+               str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") in
       hov 1 (pr_locality local ++ str"Strategy" ++ spc() ++
              hv 0 (prlist_with_sep sep pr_line l))
   | VernacUnsetOption (l,na) ->
@@ -870,7 +873,7 @@ let rec pr_vernac = function
       let pr_mayeval r c = match r with 
       | Some r0 ->
           hov 2 (str"Eval" ++ spc() ++
-          pr_red_expr (pr_constr,pr_lconstr,pr_or_by_notation pr_reference) r0 ++
+          pr_red_expr (pr_constr,pr_lconstr,pr_smart_global) r0 ++
           spc() ++ str"in" ++ spc () ++ pr_constr c)
       | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) 
       in 
@@ -891,41 +894,39 @@ let rec pr_vernac = function
 	| PrintGraph -> str"Print Graph"
 	| PrintClasses -> str"Print Classes"
 	| PrintTypeClasses -> str"Print TypeClasses"
-	| PrintInstances qid -> str"Print Instances" ++ spc () ++ pr_reference qid
+	| PrintInstances qid -> str"Print Instances" ++ spc () ++ pr_smart_global qid
 	| PrintLtac qid -> str"Print Ltac" ++ spc() ++ pr_reference qid
 	| PrintCoercions -> str"Print Coercions"
 	| PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t
 	| PrintCanonicalConversions -> str"Print Canonical Structures"
 	| PrintTables -> str"Print Tables"
-	| PrintOpaqueName qid -> str"Print Term" ++ spc() ++ pr_reference qid
 	| PrintHintGoal -> str"Print Hint"
-	| PrintHint qid -> str"Print Hint" ++ spc() ++ pr_reference qid
+	| PrintHint qid -> str"Print Hint" ++ spc() ++ pr_smart_global qid
 	| PrintHintDb -> str"Print Hint *"
 	| PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s
 	| PrintRewriteHintDbName s -> str"Print Rewrite HintDb" ++ spc() ++ str s
 	| PrintUniverses fopt -> str"Dump Universes" ++ pr_opt str fopt
-	| PrintName qid -> str"Print" ++ spc()  ++ pr_reference qid
+	| PrintName qid -> str"Print" ++ spc()  ++ pr_smart_global qid
 	| PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid
 	| PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid
 	| PrintInspect n -> str"Inspect" ++ spc() ++ int n
 	| PrintScopes -> str"Print Scopes"
 	| PrintScope s -> str"Print Scope" ++ spc() ++ str s 
 	| PrintVisibility s -> str"Print Visibility" ++ pr_opt str s 
-	| PrintAbout qid -> str"About" ++ spc()  ++ pr_reference qid
-	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_reference qid
+	| PrintAbout qid -> str"About" ++ spc()  ++ pr_smart_global qid
+	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_smart_global qid
 (* spiwack: command printing all the axioms and section variables used in a 
          term *)
 	| PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies")
-	    ++spc()++pr_reference qid
+	    ++ spc() ++ pr_smart_global qid
       in pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
   | VernacLocate loc -> 
       let pr_locate =function
-	| LocateTerm qid ->  pr_reference qid
+	| LocateTerm qid -> pr_smart_global qid
 	| LocateFile f -> str"File" ++ spc() ++ qs f
 	| LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid
 	| LocateModule qid -> str"Module" ++ spc () ++ pr_module qid
-	| LocateNotation s -> qs s
       in str"Locate" ++ spc() ++ pr_locate loc
   | VernacComments l ->
       hov 2
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 9e6ff72d31..0518da327b 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -619,8 +619,7 @@ let print_sec_context sec =
 let print_sec_context_typ sec =
   print_context false None (read_sec_context sec)
 
-let print_name ref = 
-  match locate_any_name ref with
+let print_any_name = function
   | Term (ConstRef sp) -> print_constant_with_infos sp
   | Term (IndRef (sp,_)) -> print_inductive sp
   | Term (ConstructRef ((sp,_),_)) -> print_inductive sp
@@ -639,6 +638,14 @@ let print_name ref =
     errorlabstrm
       "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
+let print_name = function
+  | Genarg.ByNotation (loc,ntn,sc) ->
+      print_any_name
+        (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) 
+               ntn sc))
+  | Genarg.AN ref ->
+      print_any_name (locate_any_name ref)
+
 let print_opaque_name qid = 
   let env = Global.env () in
   match global qid with
@@ -657,8 +664,7 @@ let print_opaque_name qid =
         let (_,c,ty) = lookup_named id env in 
 	print_named_decl (id,c,ty)
 
-let print_about ref = 
-  let k = locate_any_name ref in
+let print_about_any k =
   begin match k with
   | Term ref ->
       print_ref false ref ++ fnl () ++ print_name_infos ref ++ 
@@ -670,8 +676,16 @@ let print_about ref =
   ++
   hov 0 (str "Expands to: " ++ pr_located_qualid k)
 
+let print_about = function
+  | Genarg.ByNotation (loc,ntn,sc) ->
+      print_about_any
+        (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) 
+               ntn sc))
+  | Genarg.AN ref ->
+      print_about_any (locate_any_name ref)
+
 let print_impargs ref =
-  let ref = Nametab.global ref in
+  let ref = Smartlocate.smart_global ref in
   let impl = implicits_of_global ref in
   let has_impl = List.filter is_status_implicit impl <> [] in
   (* Need to reduce since implicits are computed with products flattened *)
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 88b0a80ecc..ba1977e893 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -18,6 +18,7 @@ open Environ
 open Reductionops
 open Libnames
 open Nametab
+open Genarg
 (*i*)
 
 (* A Pretty-Printer for the Calculus of Inductive Constructions. *)
@@ -40,10 +41,10 @@ val print_eval :
 (* This function is exported for the graphical user-interface pcoq *)
 val build_inductive : mutual_inductive -> int ->
   global_reference * rel_context * types * identifier array * types array
-val print_name : reference -> std_ppcmds
+val print_name : reference or_by_notation -> std_ppcmds
 val print_opaque_name : reference -> std_ppcmds
-val print_about : reference -> std_ppcmds
-val print_impargs : reference -> std_ppcmds
+val print_about : reference or_by_notation -> std_ppcmds
+val print_impargs : reference or_by_notation -> std_ppcmds
 
 (*i
 val print_extracted_name : identifier -> std_ppcmds