X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconSync.ml;h=ed243fe196c48a9ff5e7499f7bdce28ed91e0432;hb=3323758b99384afb5c7a70aa31bc006a78af64dd;hp=30031943d9bb1897a5fa4a2a0dc473a715b7c796;hpb=fc4cf455977934bd737c3d6c8675ef7663a6a588;p=helm.git

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index 30031943d..ed243fe19 100644
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -83,13 +83,13 @@ 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 = 
 struct
   type t = CicNotation.notation_id
-  let compare = Pervasives.compare
+  let compare =  CicNotation.compare_notation_id
 end
 
 module IdSet  = Set.Make (OrderedId)
@@ -109,3 +109,5 @@ let time_travel ~present ~past =
   in
    List.iter CicNotation.remove_notation notation_to_remove
 
+let push () = CicNotation.push ();;
+let pop () = CicNotation.pop ();;