X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitacLib.ml;h=9cc063271d801902cd5375661e5a850458fe9424;hb=49430a1d657ec9521619ea35fe911b598f055df9;hp=3acfadfb66f6e0e434e83585bbe9302964ae555f;hpb=47b36a8d040720c79d51ae7a800cbe91db4bcc4b;p=helm.git

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 3acfadfb6..9cc063271 100644
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -88,7 +88,7 @@ let fname () =
   Arg.parse arg_spec add_script usage;
   match !acc with
   | [x] -> x
-  | _ -> prerr_endline usage; exit 1
+  | _ -> print_endline usage; exit 1
 
 let pp_ocaml_mode () = 
   MatitaLog.message "";
@@ -137,6 +137,7 @@ let go () =
   CicNotation.load_notation BuildTimeConf.core_notation_script;
   Http_getter.init ();
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+  MatitaDb.create_owner_environment ();
   CicEnvironment.set_trust (* environment trust *)
     (let trust = Helm_registry.get_bool "matita.environment_trust" in
      fun _ -> trust);
@@ -148,7 +149,9 @@ let dump_moo_to_file file moo =
  let os = open_out (MatitaMisc.obj_file_of_script file) in
  let output s = output_string os s in
  output "(* GENERATED FILE: DO NOT EDIT! *)\n\n";
- List.iter output (List.rev moo);
+ List.iter
+  (fun cmd -> output (GrafiteAstPp.pp_command cmd ^ "\n"))
+  (List.rev moo);
  close_out os
   
 let main ~mode =