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
---
 parsing/printer.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'parsing')

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 3e664806d1..76c0995a5d 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -26,12 +26,7 @@ let emacs_str s = if !Options.print_emacs then s else ""
 
 let dfltpr ast = [< 'sTR"#GENTERM " ; print_ast ast >];;
 
-let pr_global 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_id (id_of_global (Global.env()) ref) in
-  [< 'sTR s >]
+let pr_global ref = pr_global_env (Global.env()) ref
 
 let global_const_name sp =
   try pr_global (ConstRef sp)
-- 
cgit v1.2.3