matitac now compiles like make (recorsively) if needed.

[helm.git] / matita / matitaprover.ml

diff --git a/matita/matitaprover.ml b/matita/matitaprover.ml
index 7a6503ab36e7f15c2730770ce5c55d3aa7a3d504..79ab7683b04acbd045d140cfcf3e65eef04e6ce1 100644 (file)
--- a/matita/matitaprover.ml
+++ b/matita/matitaprover.ml
@@ -104,7 +104,7 @@ let main () =
   in
 (*   prerr_endline data; *)
   let is = Ulexing.from_utf8_string data in
-  let gs = GrafiteSync.init () in
+  let gs = GrafiteSync.init "cic:/TPTP/" in
   let ls = 
     CicNotation2.load_notation ~include_paths:[] 
       BuildTimeConf.core_notation_script 
@@ -115,7 +115,6 @@ let main () =
       MatitaEngine.eval_from_stream 
         ~first_statement_only:false 
         ~include_paths:[]
-        ~clean_baseuri:true
         ~do_heavy_checks:false
         ~prompt:false
         ls gs is