From 2cbf0f8fe0929d36391a8f12e32873eb3a95d7cd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Aug 2009 12:15:30 +0000
Subject: Fixed incorrect optimization in Prettyp.pr_located_qualid introduced
 in commit r12265. Add a few synonyms back in Libnames/Nameops to maintain
 some minimal compatibility.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12267 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/prettyp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 538828fca2..9e6ff72d31 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -205,7 +205,7 @@ let pr_located_qualid = function
 	| IndRef _ -> "Inductive"
 	| ConstructRef _ -> "Constructor"
 	| VarRef _ -> "Variable" in
-      str ref_str ++ spc () ++ pr_global ref
+      str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref)
   | Syntactic kn ->
       str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn)
   | Dir dir ->
-- 
cgit v1.2.3