New sets of.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
index 2bae037c1b10438068ca7e1b7ade09144a20e953..50c3bd208d2b1c4465b0da542a9ecdbe8a72f803 100644 (file)
--- 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

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.mli b/helm/software/components/ng_refiner/nDiscriminationTree.mli
index 3718114a0b638bd00cb31556ea52908e83817ec5..ef977667592db10243e51e6320d6a241e4a4c3d3 100644 (file)
--- a/helm/software/components/ng_refiner/nDiscriminationTree.mli
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.mli
@@ -27,6 +27,7 @@ module NCicIndexable : Discrimination_tree.Indexable
 with type input = NCic.term and type constant_name = NReference.reference
 
 module TermSet : Set.S with type elt = NCic.term
+module TermListSet : Set.S with type elt = NCic.term list
 
 module DiscriminationTree : Discrimination_tree.DiscriminationTree 
 with type constant_name = NCicIndexable.constant_name