From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 parsing/search.mli | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'parsing/search.mli')

diff --git a/parsing/search.mli b/parsing/search.mli
index 8ee708bc..7d12d26f 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: search.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: search.mli 11739 2009-01-02 19:33:19Z herbelin $ i*)
 
 open Pp
 open Names
@@ -19,13 +19,14 @@ open Nametab
 (*s Search facilities. *)
 
 type glob_search_about_item =
-  | GlobSearchRef of global_reference
+  | GlobSearchSubPattern of constr_pattern
   | GlobSearchString of string
 
 val search_by_head : global_reference -> dir_path list * bool -> unit
 val search_rewrite : constr_pattern -> dir_path list * bool -> unit
 val search_pattern : constr_pattern -> dir_path list * bool -> unit
-val search_about  : glob_search_about_item list -> 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.
    It can be passed as argument to the raw search functions.
@@ -46,4 +47,4 @@ 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) -> 
-      glob_search_about_item list -> unit
+      (bool * glob_search_about_item) list -> unit
-- 
cgit v1.2.3