Extension de Locate

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

1 files changed, 22 insertions, 3 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 765e55b37..3cc8cea3a 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -132,8 +132,8 @@ let pr_located_qualid = function
 	| VarRef _ -> "Variable" in
       str ref_str ++ spc () ++ pr_sp (Nametab.sp_of_global ref)
   | Syntactic kn ->
-      str "Syntactic Definition" ++ spc () ++
-      pr_sp (Nametab.sp_of_syntactic_definition kn)
+      str (if !Options.v7 then "Syntactic Definition" else "Notation") ++ 
+      spc () ++ pr_sp (Nametab.sp_of_syntactic_definition kn)
   | Dir dir ->
       let s,dir = match dir with
 	| DirOpenModule (dir,_) -> "Open Module", dir
@@ -149,7 +149,26 @@ let pr_located_qualid = function
       pr_qualid qid ++ str " is not a defined object"
 
 let print_located_qualid ref =
-  hov 0 (pr_located_qualid (locate_any_name ref))
+  let (loc,qid) = qualid_of_reference ref in
+  let module N = Nametab in
+  let expand = function
+    | TrueGlobal ref -> Term ref, N.shortest_qualid_of_global Idset.empty ref
+    | SyntacticDef kn -> Syntactic kn, N.shortest_qualid_of_syndef kn in
+  match List.map expand (N.extended_locate_all qid) with
+    | [] -> 
+	let (dir,id) = repr_qualid qid in
+	if dir = empty_dirpath then
+	  str "No object of basename " ++ pr_id id
+	else
+	  str "No object of suffix " ++ pr_qualid qid
+    | l ->
+	prlist_with_sep fnl
+	(fun (o,oqid) ->
+	  hov 2 (pr_located_qualid o ++
+	  (if oqid <> qid then
+	    spc() ++ str "(visible as " ++ pr_qualid oqid ++ str")"
+	  else
+	    mt ()))) l
 
 (******************************************)
 (**** Printing declarations and judgments *)