- Grammar for all obj commands ported to NG (let recs and inductives still need

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

diff --git a/helm/software/components/grafite_parser/print_grammar.ml b/helm/software/components/grafite_parser/print_grammar.ml
index d2eb817adce30991523ee61908d9180cf51764b3..bb2a68b326ae39bf631c095dcb58d1fadce6f11e 100644 (file)
--- a/helm/software/components/grafite_parser/print_grammar.ml
+++ b/helm/software/components/grafite_parser/print_grammar.ml
@@ -263,7 +263,7 @@ let rec visit_entries fmt todo pped =
 ;;
 
 let ebnf_of_term () =
-  let g_entry = Grammar.Entry.obj CicNotationParser.term in
+  let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in
   let buff = Buffer.create 100 in
   let fmt = Format.formatter_of_buffer buff in
   visit_entries fmt [g_entry] [];