aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/search.mli
blob: 42e277a5d1c175d1aa42cee3d56d396970212330 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

(* $Id$ *)

open Pp
open Term
open Environ
open Pattern

(*s Search facilities. *)

val crible : (std_ppcmds -> env -> constr -> unit) -> global_reference -> unit

val search_by_head : global_reference -> unit

val search_modules : global_reference -> string list * string -> unit
val search_rewrite : Pattern.constr_pattern  -> string list * string -> unit
val search_pattern : Pattern.constr_pattern  -> string list * string -> unit