- cleanup

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 6da952c7d2ada70e80cc973925c747d7d07a25fd..27634f1c3ddbf8b3afd311417d66b986abc4fb93 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -28,8 +28,6 @@
 module N  = NotationPt
 module G  = GrafiteAst
 
-type ast_statement = G.statement
-
 let exc_located_wrapper f =
   try
     f ()
@@ -619,7 +617,7 @@ EXTEND
   statement
 ;;
 
-type db = ast_statement Grammar.Entry.e ;;
+type db = GrafiteAst.statement Grammar.Entry.e ;;
 
 class type g_status =
  object

diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli
index 888b7394249b148313929ba702f09726f0a609b3..2b458fdf80f7501a6833ba0c9d7c304db74d9533 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.mli
+++ b/matita/components/grafite_parser/grafiteParser.mli
@@ -23,8 +23,6 @@
  * http://helm.cs.unibo.it/
  *)
 
-type ast_statement = GrafiteAst.statement
-
 type db 
 
 class type g_status =
@@ -49,4 +47,4 @@ val extend : #status as 'status ->
  (* never_include: do not call LexiconEngine to do includes, 
   * always raise NoInclusionPerformed *) 
 (** @raise End_of_file *)
-val parse_statement: #status -> Ulexing.lexbuf -> ast_statement
+val parse_statement: #status -> Ulexing.lexbuf -> GrafiteAst.statement