From 4c708b93f1e88f530a02f72c3f9b10f5846f4f74 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 8 Apr 2010 16:37:26 +0000 Subject: [PATCH] New sets of. From: sacerdot --- .../components/ng_refiner/nDiscriminationTree.ml | 10 ++++++++++ .../components/ng_refiner/nDiscriminationTree.mli | 1 + 2 files changed, 11 insertions(+) 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 -- 2.39.2