disambiguation even more abstracted

[helm.git] / helm / software / components / lexicon / lexiconSync.ml

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index 9010dfcff01cbdefb4e74f1080a230cbcae0f89e..ed243fe196c48a9ff5e7499f7bdce28ed91e0432 100644 (file)
--- 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 ();;