X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconSync.ml;h=ed243fe196c48a9ff5e7499f7bdce28ed91e0432;hb=1d212933a86f2820a151555516f7a53ab1c9f8e7;hp=9010dfcff01cbdefb4e74f1080a230cbcae0f89e;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index 9010dfcff..ed243fe19 100644
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -89,7 +89,7 @@ let add_aliases_for_objs =
 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 ();;