- LexiconAst merged into GrafiteAst

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

diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli
index 4e4b035abdca243abfd2d2f9baf5305ca4e0b1f6..dc39ab3166773c107124bd9fbfb13e94409ab283 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.mli
+++ b/matita/components/grafite_parser/grafiteParser.mli
@@ -29,19 +29,17 @@ type 'a localized_option =
 
 type ast_statement = GrafiteAst.statement
 
-exception NoInclusionPerformed of string (* full path *)
-
 type db 
 
 class type g_status =
  object
-  inherit LexiconEngine.g_status
+  inherit LexiconTypes.g_status
   method parser_db: db
  end
 
 class status :
  object('self)
-  inherit LexiconEngine.status
+  inherit LexiconTypes.status
   method parser_db : db
   method set_parser_db : db -> 'self
   method set_parser_status : 'status. #g_status as 'status -> 'self