From 458fdba7a34fdf49f4f93e6734e90c6603c61adf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 19 Nov 2001 09:31: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@2202 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_trees.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index c60abbc280..809fbd7b84 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -272,7 +272,7 @@ let last_of_cvt_flags (_,red) =
 	  | EvalVarRef id -> nvar id
 	  | EvalConstRef sp ->
 	      ast_of_qualid
-                (qualid_of_global (Global.env()) (ConstRef sp)))
+                (shortest_qualid_of_global (Global.env()) (ConstRef sp)))
        lconst in
    if lqid = [] then []
    else if n_unf then [ope("Delta",[]);ope("UnfBut",lqid)]
@@ -292,7 +292,8 @@ let ast_of_cvt_redexp = function
       [match sp with
 	| EvalVarRef id -> nvar id
 	| EvalConstRef sp -> 					
-	    ast_of_qualid (qualid_of_global (Global.env()) (ConstRef sp))]
+	    ast_of_qualid
+	      (shortest_qualid_of_global (Global.env()) (ConstRef sp))]
       @(List.map num locc))) l)
   | Fold l ->
     ope("Fold",List.map (fun c -> ope ("COMMAND",
-- 
cgit v1.2.3