diff options
Diffstat (limited to 'parsing/search.ml')
| -rw-r--r-- | parsing/search.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |