X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnDiscriminationTree.ml;h=50c3bd208d2b1c4465b0da542a9ecdbe8a72f803;hb=72e835f5e6848c09faf6343fb7e276c88bfc1f2e;hp=2bae037c1b10438068ca7e1b7ade09144a20e953;hpb=2b52dcc1742d2ee0616b6526e3ade1dd21ec10f3;p=helm.git

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
index 2bae037c1..50c3bd208 100644
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -34,6 +34,16 @@ end
 
 module TermSet = Set.Make(TermOT)
 
+module TermListOT : Set.OrderedType with type t = NCic.term list =
+ struct
+   type t = NCic.term list
+   let compare = Pervasives.compare
+ end
+
+module TermListSet : Set.S with type elt = NCic.term list =
+ Set.Make(TermListOT)
+
+
 module NCicIndexable : Indexable
 with type input = NCic.term 
 and type constant_name = NReference.reference = struct