milestone in basic_2, λδ-2A reconstructed

[helm.git] / helm / software / components / ng_refiner / nDiscriminationTree.ml

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