diff options
Diffstat (limited to 'parsing/search.mli')
| -rw-r--r-- | parsing/search.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/search.mli b/parsing/search.mli index 073a20f87..f7e384e96 100644 --- a/parsing/search.mli +++ b/parsing/search.mli @@ -38,3 +38,5 @@ val raw_pattern_search : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> constr_pattern -> unit val raw_search_rewrite : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> constr_pattern -> unit +val raw_search_about : (global_reference -> env -> constr -> bool) -> + (global_reference -> env -> constr -> unit) -> global_reference -> unit |