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
---
 dev/base_include | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index 711dcb2a1e..b6c2e4d08f 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -105,6 +105,8 @@ open Ppextend
 open Reserve
 open Syntax_def
 open Topconstr
+open Prettyp
+open Search
 
 open Clenvtac
 open Evar_refiner
@@ -180,7 +182,7 @@ let constr_of_string s =
 open Declarations;;
 
 let constbody_of_string s =
-  let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_sp (path_of_string s))) in
+  let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in
   Option.get b.const_body;;
 
 (* Get the current goal *)
-- 
cgit v1.2.3