1. Several files in grafite that should be in grafite_parser moved there.

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

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index 134e00e7c10011bbbdf0ea2d79eaf4be82da218a..44f6681833c40408e75dc3ec61f6ba46db95be86 100644 (file)
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -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