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

1 files changed, 19 insertions, 5 deletions

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 *)