X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconSync.ml;h=9010dfcff01cbdefb4e74f1080a230cbcae0f89e;hb=80f3756848ca8b178255f717794c5c2358d5d585;hp=d7fa27f902b2e7038ee46e7b3c9ed9986e025b47;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index d7fa27f90..9010dfcff 100644
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -41,7 +41,7 @@ let alias_diff ~from status =
     status.LexiconEngine.aliases []
 
 let alias_diff =
- let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in
+ let profiler = HExtlib.profile "alias_diff(conteg. anche in include)" in
  fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
 
 (** given a uri and a type list (the contructors types) builds a list of pairs
@@ -83,7 +83,7 @@ let add_aliases_for_object status uri =
 let add_aliases_for_objs =
  List.fold_left
   (fun status uri ->
-    let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+    let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
      add_aliases_for_object status uri obj)
  
 module OrderedId = 
@@ -109,11 +109,3 @@ let time_travel ~present ~past =
   in
    List.iter CicNotation.remove_notation notation_to_remove
 
-let init =
-  {
-    LexiconEngine.aliases = DisambiguateTypes.Environment.empty;
-    multi_aliases = DisambiguateTypes.Environment.empty;
-    lexicon_content_rev = [];
-    notation_ids = [];
-    metadata = [];
-  }