From: Claudio Sacerdoti Coen Date: Thu, 8 Apr 2010 16:37:26 +0000 (+0000) Subject: New sets of. X-Git-Tag: make_still_working~2940 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c708b93f1e88f530a02f72c3f9b10f5846f4f74;p=helm.git New sets of. From: sacerdot --- 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 diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.mli b/helm/software/components/ng_refiner/nDiscriminationTree.mli index 3718114a0..ef9776675 100644 --- 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