big change in parsing, trying to make all functional

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

diff --git a/matita/components/grafite_parser/print_grammar.mli b/matita/components/grafite_parser/print_grammar.mli
index 584a79b3e7a281fc51fded3dad4698d2f0986d04..28becba1d42f64d954fb50181439de6128df001c 100644 (file)
--- a/matita/components/grafite_parser/print_grammar.mli
+++ b/matita/components/grafite_parser/print_grammar.mli
@@ -25,4 +25,4 @@
 
 (* $Id: print_grammar.ml 6977 2006-10-25 12:41:21Z sacerdot $ *)
 
-val ebnf_of_term: unit -> string
+val ebnf_of_term: #GrafiteParser.status -> string