X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fextlib%2Fdiscrimination_tree.mli;h=bf6b071f1ca2bc98f4aeebc5738ab068dc17489c;hb=578ba04e1a0812f538729fbc02ea38d2cfd0ed3e;hp=c07715b21ccb1fcdc3514b9ed0ca970b85dde75e;hpb=79a5e6b1d8cdb73611fb57507ed9a71f7b75d014;p=helm.git

diff --git a/matita/components/extlib/discrimination_tree.mli b/matita/components/extlib/discrimination_tree.mli
index c07715b21..bf6b071f1 100644
--- a/matita/components/extlib/discrimination_tree.mli
+++ b/matita/components/extlib/discrimination_tree.mli
@@ -63,11 +63,19 @@ 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
+
+      (* the int is the number of symbools that matched, note that
+       * Collector.to_list returns a sorted list, biggest matches first. *)
+      module type Collector = sig
+        type t
+        val empty : t
+        val union : t -> t -> t
+        val inter : t -> t -> data list
+        val to_list : t -> data list
+      end
+      module Collector : Collector
+      val retrieve_generalizations_sorted : t -> input -> Collector.t
+      val retrieve_unifiables_sorted : t -> input -> Collector.t
     end