X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnDiscriminationTree.ml;h=50c3bd208d2b1c4465b0da542a9ecdbe8a72f803;hb=72e835f5e6848c09faf6343fb7e276c88bfc1f2e;hp=fff8b67699c6d5388dfa811995d30a686a5aff84;hpb=8e0e2b06cfc3fb3116e1fce632d9897fdbac9895;p=helm.git

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
index fff8b6769..50c3bd208 100644
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -34,15 +34,26 @@ 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 = NUri.uri = struct
+with type input = NCic.term 
+and type constant_name = NReference.reference = struct
 
 type input = NCic.term
-type constant_name = NUri.uri
+type constant_name = NReference.reference
 
 let ppelem = function
-  | Constant (uri,arity) -> 
-      "("^NUri.name_of_uri uri ^ "," ^ string_of_int arity^")"
+  | Constant (ref,arity) -> 
+      "("^NReference.string_of_reference ref ^ "," ^ string_of_int arity^")"
   | Bound (i,arity) -> 
       "("^string_of_int i ^ "," ^ string_of_int arity^")"
   | Variable -> "?"
@@ -67,7 +78,7 @@ let path_string_of t =
     | NCic.Rel i -> [Bound (i, arity)]
     | NCic.Sort (NCic.Prop) -> assert (arity=0); [Proposition]
     | NCic.Sort _ -> assert (arity=0); [Datatype]
-    | NCic.Const (NReference.Ref (u,_)) -> [Constant (u, arity)]
+    | NCic.Const (u) -> [Constant (u, arity)]
     | NCic.Match _ -> [Dead]
   in 
   aux 0 0 t
@@ -76,7 +87,7 @@ let path_string_of t =
 let compare e1 e2 =
   match e1,e2 with
   | Constant (u1,a1),Constant (u2,a2) -> 
-       let x = NUri.compare u1 u2 in
+       let x = NReference.compare u1 u2 in
        if x = 0 then Pervasives.compare a1 a2 else x
   | e1,e2 -> Pervasives.compare e1 e2
 ;;