diff options
Diffstat (limited to 'parsing/search.ml')
| -rw-r--r-- | parsing/search.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/parsing/search.ml b/parsing/search.ml index 28362d72..c375826c 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: search.ml 9310 2006-10-28 19:35:09Z herbelin $ *) +(* $Id: search.ml 10840 2008-04-23 21:29:34Z herbelin $ *) open Pp open Util @@ -50,17 +50,17 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = let crible_rec (sp,_) lobj = match object_tag lobj with | "VARIABLE" -> (try - let (idc,_,typ) = get_variable (basename sp) in + let (id,_,typ) = Global.lookup_named (basename sp) in if refopt = None - || head_const typ = constr_of_global (out_some refopt) + || head_const typ = constr_of_global (Option.get refopt) then - fn (VarRef idc) env typ + fn (VarRef id) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" -> 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) + || head_const typ = constr_of_global (Option.get refopt) then fn (ConstRef cst) env typ | "INDUCTIVE" -> @@ -214,7 +214,8 @@ let search_about_item (itemref,typ) = function let raw_search_about filter_modules display_function l = let filter ref' env typ = filter_modules ref' env typ && - List.for_all (search_about_item (ref',typ)) l + List.for_all (search_about_item (ref',typ)) l && + not (string_string_contains (name_of_reference ref') "_subproof") in gen_filtered_search filter display_function |