X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaEngine.ml;h=4429f963651f7e8fa9839626fb8aa955b119d0ec;hb=5e924927db28c0a5bbbaa4e56515d9afe0b1360f;hp=cd5c8344198288c08dbfd1cd471686fc1c6fad42;hpb=c881200303035c81106f09c4fafb06119a38c157;p=helm.git

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index cd5c83441..4429f9636 100644
--- 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