diff options
Diffstat (limited to 'toplevel/search.ml')
| -rw-r--r-- | toplevel/search.ml | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/toplevel/search.ml b/toplevel/search.ml index 8336b488a1..26e6416a9a 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -53,13 +53,11 @@ let iter_named_context_name_type f = List.iter (fun (nme,_,typ) -> f nme typ) (* General search over hypothesis of a goal *) let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = - try - let env = Global.env () in - let iter_hyp idh typ = fn (VarRef idh) env typ in - let evmap,e = Pfedit.get_goal_context glnum in - let pfctxt = named_context e in - iter_named_context_name_type iter_hyp pfctxt - with _ -> () + let env = Global.env () in + let iter_hyp idh typ = fn (VarRef idh) env typ in + let evmap,e = Pfedit.get_goal_context glnum in + let pfctxt = named_context e in + iter_named_context_name_type iter_hyp pfctxt (* General search over declarations *) let iter_declarations (fn : global_reference -> env -> constr -> unit) = @@ -93,8 +91,10 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) = try Declaremods.iter_all_segments iter_obj with Not_found -> () -let generic_search glnum fn = - iter_hypothesis glnum fn; +let generic_search glnumopt fn = + (match glnumopt with + | None -> () + | Some glnum -> iter_hypothesis glnum fn); iter_declarations fn (** Standard display *) @@ -156,7 +156,7 @@ let search_about_filter query gr env typ = match query with (** SearchPattern *) -let search_pattern g pat mods = +let search_pattern gopt pat mods = let ans = ref [] in let filter ref env typ = let f_module = module_filter mods ref env typ in @@ -167,7 +167,7 @@ let search_pattern g pat mods = let iter ref env typ = if filter ref env typ then plain_display ans ref env typ in - let () = generic_search g iter in + let () = generic_search gopt iter in format_display !ans (** SearchRewrite *) @@ -180,7 +180,7 @@ let rewrite_pat1 pat = let rewrite_pat2 pat = PApp (PRef eq, [| PMeta None; PMeta None; pat |]) -let search_rewrite g pat mods = +let search_rewrite gopt pat mods = let pat1 = rewrite_pat1 pat in let pat2 = rewrite_pat2 pat in let ans = ref [] in @@ -196,12 +196,12 @@ let search_rewrite g pat mods = let iter ref env typ = if filter ref env typ then plain_display ans ref env typ in - let () = generic_search g iter in + let () = generic_search gopt iter in format_display !ans (** Search *) -let search_by_head g pat mods = +let search_by_head gopt pat mods = let ans = ref [] in let filter ref env typ = let f_module = module_filter mods ref env typ in @@ -212,12 +212,12 @@ let search_by_head g pat mods = let iter ref env typ = if filter ref env typ then plain_display ans ref env typ in - let () = generic_search g iter in + let () = generic_search gopt iter in format_display !ans (** SearchAbout *) -let search_about g items mods = +let search_about gopt items mods = let ans = ref [] in let filter ref env typ = let eqb b1 b2 = if b1 then b2 else not b2 in @@ -229,7 +229,7 @@ let search_about g items mods = let iter ref env typ = if filter ref env typ then plain_display ans ref env typ in - let () = generic_search g iter in + let () = generic_search gopt iter in format_display !ans type search_constraint = @@ -333,5 +333,5 @@ let interface_search flags = let iter ref env typ = if filter_function ref env typ then print_function ref env typ in - let () = generic_search 1 iter in (* TODO: chose a goal number? *) + let () = generic_search None iter in (* TODO: chose a goal number? *) !ans |