Bug fixed: the debrujinate function (hence the one to compute objects height)

[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 d3a334a591db27453e13a2bd678a00ae63f83495..bd64cfe5d5a036b2ad0e69e0356c52a2718384af 100644 (file)
--- 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)