Propagation of changes to 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 2dc83319497c54e904e91b3fddf1667afe624743..98942e6850bc6e39020f14b07a2f35673125a68c 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.mli
+++ b/matita/components/grafite_parser/grafiteParser.mli
@@ -27,11 +27,7 @@ type 'a localized_option =
    LSome of 'a
  | LNone of GrafiteAst.loc
 
-type ast_statement =
-  (NotationPt.term, NotationPt.term,
-   NotationPt.term GrafiteAst.reduction, 
-   NotationPt.term NotationPt.obj, string)
-    GrafiteAst.statement
+type ast_statement = GrafiteAst.statement
 
 exception NoInclusionPerformed of string (* full path *)