From 2cbf0f8fe0929d36391a8f12e32873eb3a95d7cd Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
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
---
 library/libnames.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'library/libnames.ml')

diff --git a/library/libnames.ml b/library/libnames.ml
index 21be8f7d1..c7d484d1e 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -289,3 +289,8 @@ let pop_global_reference = function
   | IndRef (kn,i) -> IndRef (pop_kn kn,i)
   | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
   | VarRef id -> anomaly "VarRef not poppable"
+
+(* Deprecated synonyms *)
+
+let make_short_qualid = qualid_of_ident
+let qualid_of_sp = qualid_of_path
-- 
cgit v1.2.3