irediced usage of matita.includes, that is now set by

[helm.git] / components / grafite_parser / grafiteWalker.mli

diff --git a/components/grafite_parser/grafiteWalker.mli b/components/grafite_parser/grafiteWalker.mli
index b4ca6f0d73dad127382cd825b3abe07deb747c0d..c9df8ab487820802545c320d76d387ed5e21329f 100644 (file)
--- a/components/grafite_parser/grafiteWalker.mli
+++ b/components/grafite_parser/grafiteWalker.mli
@@ -33,7 +33,9 @@ type statement_test =
 val grep_statement:
   ?status: LexiconEngine.status ->
   ?callback: (string -> unit) ->
-  fname:string -> statement_test ->
+  fname:string -> 
+  include_paths: string list ->
+  statement_test ->
     string list
 
   (** As above, but act on all file (recursively) located under directory
@@ -43,6 +45,8 @@ val grep_statement:
 val rgrep_statement:
   ?status: LexiconEngine.status ->
   ?callback: (string * string -> unit) ->
-  ?fname_test:(string -> bool) -> dirname:string -> statement_test ->
+  ?fname_test:(string -> bool) -> dirname:string -> 
+  include_paths: string list ->        
+  statement_test ->
     (string * string) list