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

(*i $Id$ i*)

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