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

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