Matitaweb:

[helm.git] / matitaB / components / ng_disambiguation / grafiteDisambiguate.ml

diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index b1dc98a1e23e46cde8c3e265fed0061327a2af2b..544128befd29ea706c6247c50e2056f38b08ee8b 100644 (file)
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -297,7 +297,7 @@ let diff_obj loc o1 o2 = match o1,o2 with
 let rec find_diffs l =
   let loc,_ = List.hd (List.hd l) in
   let hds = List.map (fun x -> snd (List.hd x)) l in
-  let uniq_hds = HExtlib.list_uniq hds in
+  let uniq_hds = HExtlib.list_uniq (List.sort Pervasives.compare hds) in
 
   if List.length uniq_hds > 1
     then loc, uniq_hds