More progress in technicalities/setoids.ma.

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

diff --git a/components/grafite_parser/grafiteParser.mli b/components/grafite_parser/grafiteParser.mli
index cb88940ffde19daea908157bc497b83acc0c4a3b..f38f0e5dc3e4dde8a76ee9e95c5b5a141c94ad03 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 =
@@ -37,6 +38,9 @@ type statement =
   LexiconEngine.status ->
     LexiconEngine.status * ast_statement localized_option
 
+(* this callback is called on every lexicon command *)
+val set_callback: (LexiconAst.command -> unit) -> unit 
+
 val parse_statement: Ulexing.lexbuf -> statement  (** @raise End_of_file *)
 
 val statement: statement Grammar.Entry.e