From 57b4083c0bae139d35433d68d5a73f3cefb53635 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 16 Feb 2001 15:10:54 +0000
Subject: Suppression sp_of_id

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1392 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/search.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/parsing/search.ml b/parsing/search.ml
index 23905a7dd1..fc2100a6a3 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -132,7 +132,9 @@ let filtered_search filter_function display_function ref =
 
 let rec id_from_pattern = function
   | PRef gr -> gr
-  | PVar id -> Nametab.sp_of_id CCI id
+(* should be appear as a PRef (VarRef sp) !!
+  | PVar id -> Nametab.locate (make_qualid [] (string_of_id id))
+ *)
   | PApp (p,_) -> id_from_pattern p
   | _ -> error "the pattern is not simple enough"
 	
-- 
cgit v1.2.3