X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnDiscriminationTree.ml;h=bd64cfe5d5a036b2ad0e69e0356c52a2718384af;hb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;hp=d3a334a591db27453e13a2bd678a00ae63f83495;hpb=6e785555b301cc1abe1671de3bd970aebebce71a;p=helm.git

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
index d3a334a59..bd64cfe5d 100644
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -24,10 +24,22 @@
  *)
 
 (* $Id$ *)
-(*
-module NCicIndexable : Discrimination_tree.Indexable
+
+open Discrimination_tree
+
+module TermOT : Set.OrderedType with type t = NCic.term = struct 
+  type t = NCic.term 
+  let compare = Pervasives.compare 
+end
+
+module TermSet = Set.Make(TermOT)
+
+module NCicIndexable : Indexable
 with type input = NCic.term and type constant_name = NUri.uri = struct
 
+type input = NCic.term
+type constant_name = NUri.uri
+
 let ppelem = function
   | Constant (uri,arity) -> 
       "("^NUri.name_of_uri uri ^ "," ^ string_of_int arity^")"
@@ -71,6 +83,4 @@ let string_of_path l = String.concat "." (List.map ppelem l) ;;
 
 end
 
-module DiscriminationTree = 
-  Discrimination_tree.DiscriminationTreeIndexing(NCicIndexable)
-  *)
+module DiscriminationTree = Make(NCicIndexable)(TermSet)