diff options
Diffstat (limited to 'toplevel/search.mli')
| -rw-r--r-- | toplevel/search.mli | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/toplevel/search.mli b/toplevel/search.mli index cc764fbde..a9d62c6ef 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -1,10 +1,10 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) @@ -16,7 +16,7 @@ open Pattern open Libnames open Nametab -(*s Search facilities. *) +(** {6 Search facilities. } *) type glob_search_about_item = | GlobSearchSubPattern of constr_pattern @@ -28,14 +28,14 @@ val search_pattern : constr -> dir_path list * bool -> unit val search_about : (bool * glob_search_about_item) list -> dir_path list * bool -> unit -(* The filtering function that is by standard search facilities. +(** The filtering function that is by standard search facilities. It can be passed as argument to the raw search functions. It is used in pcoq. *) val filter_by_module_from_list : dir_path list * bool -> global_reference -> env -> 'a -> bool -(* raw search functions can be used for various extensions. +(** raw search functions can be used for various extensions. They are also used for pcoq. *) val gen_filtered_search : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> unit |