X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitacLib.ml;h=d1962c99d74c6beea27c41990009c3324529546c;hb=f4460413546165a7fabbf1e1da4cf2f5a44b26b9;hp=23a0ca15fa2cc3c22ce4effa407d0a7ab44c7bec;hpb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;p=helm.git

diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml
index 23a0ca15f..d1962c99d 100644
--- a/matita/matita/matitacLib.ml
+++ b/matita/matita/matitacLib.ml
@@ -29,7 +29,7 @@ open Printf
 
 open GrafiteTypes
 
-exception AttemptToInsertAnAlias of LexiconTypes.status
+exception AttemptToInsertAnAlias of GrafiteDisambiguate.status
 
 let slash_n_RE = Pcre.regexp "\\n" ;;
 
@@ -122,13 +122,10 @@ 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 GrafiteDisambiguate.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
+   (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
@@ -175,7 +172,7 @@ let compile atstart options fname =
       | [] -> grafite_status
       | (g,None)::_ -> g
       | (g,Some _)::_ ->
-         raise (AttemptToInsertAnAlias (g :> LexiconTypes.status))
+         raise (AttemptToInsertAnAlias (g :> GrafiteDisambiguate.status))
      in
        aux_for_dump print_cb grafite_status
     in