X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_parser%2FgrafiteParser.mli;h=6a1980011409c790625df02005b9cb17d70c26ae;hb=1a40d93d10be4ee71ae9474384af931d70918690;hp=7b33c6e4234809b64f4ed0a3d373b318dc4e4c65;hpb=a696aae5ea794cd43fd3d83d37a0345d2a1387b3;p=helm.git

diff --git a/helm/ocaml/grafite_parser/grafiteParser.mli b/helm/ocaml/grafite_parser/grafiteParser.mli
index 7b33c6e42..6a1980011 100644
--- a/helm/ocaml/grafite_parser/grafiteParser.mli
+++ b/helm/ocaml/grafite_parser/grafiteParser.mli
@@ -23,15 +23,19 @@
  * http://helm.cs.unibo.it/
  *)
 
+type 'a localized_option =
+   LSome of 'a
+ | LNone of Token.flocation
+
 type statement =
-  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
-   CicNotationPt.obj, string)
-    GrafiteAst.statement
+ include_paths:string list ->
+ LexiconEngine.status ->
+  LexiconEngine.status *
+  (CicNotationPt.term, CicNotationPt.term,
+   CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
+    GrafiteAst.statement localized_option
 
 val parse_statement: Ulexing.lexbuf -> statement  (** @raise End_of_file *)
 
-  (** @raise End_of_file *)
-val parse_dependencies: Ulexing.lexbuf -> GrafiteAst.dependency list
-
 val statement: statement Grammar.Entry.e