* http://cs.unibo.it/helm/.
*)
-(*
module NCicIndexable : Discrimination_tree.Indexable
-with type input = NCic.term and type constant_name = NUri.uri
+with type input = NCic.term and type constant_name = NReference.reference
-module DiscriminationTree :
- Discrimination_tree.DiscriminationTreeIndexing(NCicIndexable)
-*)
+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
+and type input = NCicIndexable.input
+and type data = TermSet.elt and type dataset = TermSet.t