Constants are indexed using the Reference, not the Uri, so that constructors

are different!

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
index fff8b67699c6d5388dfa811995d30a686a5aff84..2bae037c1b10438068ca7e1b7ade09144a20e953 100644 (file)
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -35,14 +35,15 @@ end
 module TermSet = Set.Make(TermOT)
 
 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 +68,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 +77,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
 ;;