snapshot, notably:

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 49488a94dfe3fe38bb5d593933df741f7e6bfe93..20111286e12f2c8aacf7e440a794bf37dd508d5e 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -55,6 +55,7 @@ let dbd =
     ~user:(Helm_registry.get "db.user")
     ~database:(Helm_registry.get "db.database")
     ()
+let _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.owner")
 let gui = MatitaGui.instance ()
 let disambiguator =
   new MatitaDisambiguator.disambiguator ~parserr ~dbd
@@ -114,7 +115,7 @@ let proof_handler =
   }
 
 let interpreter =
-  let console = gui#console in
+  let console = (gui#console :> MatitaTypes.console) in
   new MatitaInterpreter.interpreter
     ~disambiguator ~proof_handler ~console ~dbd ()
 
@@ -222,6 +223,10 @@ let _ =
         (not (Helm_registry.get_bool "matita.auto_disambiguation")));
     addDebugItem "dump proof status to stdout" (fun _ ->
       print_endline ((get_proof ())#toString));
+    addDebugItem "dump environment to \"env.dump\"" (fun _ ->
+      let oc = open_out "env.dump" in
+      CicEnvironment.dump_to_channel oc;
+      close_out oc);
     addDebugItem "print selected terms" (fun () ->
       let i = ref 0 in
       List.iter