Huge reorganization of matita and ocaml.

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

diff --git a/helm/ocaml/grafite_parser/grafiteParser.mli b/helm/ocaml/grafite_parser/grafiteParser.mli
index 7b33c6e4234809b64f4ed0a3d373b318dc4e4c65..6a1980011409c790625df02005b9cb17d70c26ae 100644 (file)
--- 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