now destruct takes an optional list of term rather than a sigle optional term

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

diff --git a/components/grafite_parser/grafiteParser.mli b/components/grafite_parser/grafiteParser.mli
index cb88940ffde19daea908157bc497b83acc0c4a3b..f8754df0c4715f14c098e9072310e7d53be25a86 100644 (file)
--- a/components/grafite_parser/grafiteParser.mli
+++ b/components/grafite_parser/grafiteParser.mli
@@ -29,7 +29,8 @@ type 'a localized_option =
 
 type ast_statement =
   (CicNotationPt.term, CicNotationPt.term,
-   CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
+   CicNotationPt.term GrafiteAst.reduction, 
+   CicNotationPt.term CicNotationPt.obj, string)
     GrafiteAst.statement
 
 type statement =
@@ -41,3 +42,5 @@ val parse_statement: Ulexing.lexbuf -> statement  (** @raise End_of_file *)
 
 val statement: statement Grammar.Entry.e
 
+(* this callback is called on every include command *)
+val set_callback: (string -> unit) -> unit