big change in parsing, trying to make all functional

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

diff --git a/matita/components/grafite_parser/print_grammar.ml b/matita/components/grafite_parser/print_grammar.ml
index 893a3f53c9ef2a72e93f57d7ed9187e7901ad18a..5bc87f247296fba632b30781bcef587f4a6256b3 100644 (file)
--- a/matita/components/grafite_parser/print_grammar.ml
+++ b/matita/components/grafite_parser/print_grammar.ml
@@ -264,8 +264,8 @@ let rec visit_entries fmt todo pped =
       visit_entries fmt todo pped
 ;;
 
-let ebnf_of_term () =
-  let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in
+let ebnf_of_term status =
+  let g_entry = Grammar.Entry.obj (CicNotationParser.term status) in
   let buff = Buffer.create 100 in
   let fmt = Format.formatter_of_buffer buff in
   visit_entries fmt [g_entry] [];