rebuilt

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

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index bb796db1e79d8f005630d227cfacd8bdee3437a7..c29b507792f698035809c66bd055827b85e4044b 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -72,16 +72,18 @@ 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 owner = (Helm_registry.get "matita.owner") ;;
+let _ = MetadataTypes.ownerize_tables owner ;;
+let _ = MatitaDb.clean_owner_environment dbd owner ;; 
+let _ = MatitaDb.create_owner_environment dbd owner ;; 
+
 let disambiguator =
   new MatitaDisambiguator.disambiguator ~parserr ~dbd
     ~chooseUris:mono_uris_callback ~chooseInterp:mono_interp_callback
     ()
 let console = new tty_console
-let currentProof = (new MatitaProof.currentProof :> MatitaTypes.currentProof)
-let interpreter =
-  new MatitaInterpreter.interpreter
-    ~disambiguator ~currentProof ~console ~dbd ()
+let interpreter = MatitaInterpreter.interpreter ~disambiguator ~console ()
 
 let run_script fname =
   message (sprintf "execution of %s started:" fname);