BIG BUG FIXED (???): in place of using Grammar.Entry.parse we should have

[helm.git] / matita / matita / matitaEngine.ml

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index cd5c8344198288c08dbfd1cd471686fc1c6fad42..4429f963651f7e8fa9839626fb8aa955b119d0ec 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -249,7 +249,11 @@ and compile ~compiling ~include_paths fname =
         (Filename.dirname 
           (Http_getter.filename ~local:true ~writable:true (baseuri ^
           "foo.con")));
-    let buf = Ulexing.from_utf8_channel (open_in fname) in
+    let grammar = CicNotationParser.level2_ast_grammar grafite_status in
+    let buf =
+     Grammar.parsable grammar
+      (Obj.magic (Ulexing.from_utf8_channel (open_in fname)))
+    in
     let print_cb =
       if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
       else pp_ast_statement