Re-installation de l'affichage des globaux par des noms courts

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

1 files changed, 8 insertions, 1 deletions

diff --git a/library/nametab.ml b/library/nametab.ml
index 9348ff30d..f70d672f8 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -280,7 +280,7 @@ let exists_section dir =
 
 (* For a sp Coq.A.B.x, try to find the shortest among x, B.x, A.B.x
    and Coq.A.B.x is a qualid that denotes the same object. *)
-let qualid_of_global env ref =  
+let shortest_qualid_of_global env ref =  
   let sp = sp_of_global env ref in
   let (pth,id) = repr_path sp in
   let rec find_visible dir qdir =
@@ -292,6 +292,13 @@ let qualid_of_global env ref =
   in
   find_visible (repr_dirpath pth) (make_dirpath [])
 
+let pr_global_env env ref =
+  (* Il est important de laisser le let-in, car les streams s'évaluent
+  paresseusement : il faut forcer l'évaluation pour capturer
+  l'éventuelle levée d'une exception (le cas échoit dans le debugger) *)
+  let s = string_of_qualid (shortest_qualid_of_global env ref) in
+  [< 'sTR s >]
+
 (********************************************************************)
 
 (********************************************************************)