From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 parsing/search.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'parsing/search.ml')

diff --git a/parsing/search.ml b/parsing/search.ml
index 995aa953..28362d72 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: search.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
+(* $Id: search.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
 
 open Pp
 open Util
@@ -57,12 +57,12 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
 	     fn (VarRef idc) env typ
 	 with Not_found -> (* we are in a section *) ())
     | "CONSTANT" ->
-	let kn = locate_constant (qualid_of_sp sp) in
-	let {const_type=typ} = Global.lookup_constant kn in
+	let cst = locate_constant (qualid_of_sp sp) in
+	let typ = Typeops.type_of_constant env cst in
         if refopt = None
 	  || head_const typ = constr_of_global (out_some refopt)
 	then
-	  fn (ConstRef kn) env typ
+	  fn (ConstRef cst) env typ
     | "INDUCTIVE" -> 
 	let kn = locate_mind (qualid_of_sp sp) in
         let mib = Global.lookup_mind kn in 
-- 
cgit v1.2.3