notation kind of works

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

diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml
index 23a0ca15fa2cc3c22ce4effa407d0a7ab44c7bec..cf037531fa73fb5d401ce08e83c023cc02b48cc2 100644 (file)
--- a/matita/matita/matitacLib.ml
+++ b/matita/matita/matitacLib.ml
@@ -122,10 +122,7 @@ let compile atstart options fname =
     Librarian.baseuri_of_script ~include_paths fname in
   if Http_getter_storage.is_read_only baseuri then assert false;
   activate_extraction baseuri fname ;
-  let lexicon_status = 
-    CicNotation2.load_notation ~include_paths:[] (new LexiconTypes.status)
-      BuildTimeConf.core_notation_script 
-  in
+  let lexicon_status = new LexiconTypes.status in
   atstart (); (* FG: do not invoke before loading the core notation script *)  
   let grafite_status =
    (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in