From 7d8a167b36d1f27cc38f3b042eb6f2c01a8b6177 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 19 Nov 2001 08:40:40 +0000 Subject: 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 --- library/nametab.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'library/nametab.ml') 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 >] + (********************************************************************) (********************************************************************) -- cgit v1.2.3