From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 7 Jan 2011 22:01:00 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~2602
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=79a5e6b1d8cdb73611fb57507ed9a71f7b75d014;p=helm.git

...
---

diff --git a/matita/components/extlib/discrimination_tree.ml b/matita/components/extlib/discrimination_tree.ml
index 4caf38de1..d69228b0c 100644
--- a/matita/components/extlib/discrimination_tree.ml
+++ b/matita/components/extlib/discrimination_tree.ml
@@ -184,7 +184,7 @@ and type data = A.elt and type dataset = A.t =
 
       module O = struct
         type t = A.t * int
-        let compare (_,a) (_,b) = compare a b
+        let compare (_,a) (_,b) = compare b a
       end
       module S = Set.Make(O)
 
diff --git a/matita/components/extlib/discrimination_tree.mli b/matita/components/extlib/discrimination_tree.mli
index 95e33d6ad..c07715b21 100644
--- a/matita/components/extlib/discrimination_tree.mli
+++ b/matita/components/extlib/discrimination_tree.mli
@@ -63,6 +63,9 @@ module type DiscriminationTree  =
       val in_index : t -> input -> (data -> bool) -> bool
       val retrieve_generalizations : t -> input -> dataset
       val retrieve_unifiables : t -> input -> dataset
+      (* the int is the number of symbools that matched, the list
+       * is sorted with biggest matches first. the same data may match
+       * twice, and thus appear twice with different number of matches *)
       val retrieve_generalizations_sorted : t -> input -> (data * int) list
       val retrieve_unifiables_sorted : t -> input -> (data * int) list
     end