From 79a5e6b1d8cdb73611fb57507ed9a71f7b75d014 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 7 Jan 2011 22:01:00 +0000 Subject: [PATCH] ... --- matita/components/extlib/discrimination_tree.ml | 2 +- matita/components/extlib/discrimination_tree.mli | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) 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 -- 2.39.2