Big commit to let Ferruccio try the merge_coercion patch.

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

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index d0127530870c0e53295f25eb67e0a2c88d736056..44f6681833c40408e75dc3ec61f6ba46db95be86 100644 (file)
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -65,7 +65,7 @@ let initialize_db init_status =
   if not (already_configured [ Db ] init_status) then
     begin
       MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
-      MatitaDb.create_owner_environment ();
+      LibraryDb.create_owner_environment ();
       Db::init_status
     end
   else
@@ -85,7 +85,7 @@ let initialize_notation init_status =
   wants [ConfigurationFile] init_status;
   if not (already_configured [Notation] init_status) then
     begin
-      CicNotation.load_notation BuildTimeConf.core_notation_script;
+      CicNotation2.load_notation BuildTimeConf.core_notation_script;
       Notation::init_status
     end
   else