diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
| tree | 591e9e512063e34099782e2518573f15ffeac003 /parsing/search.ml | |
| parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) | |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
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 |