From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 4 Mar 2010 08:27:05 +0000 (+0000)
Subject: In line with the ml.
X-Git-Tag: make_still_working~3014
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8d6963c2cd6273fe60733ba3094e9567a17e5c51;p=helm.git

In line with the ml.
---

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.mli b/helm/software/components/ng_refiner/nDiscriminationTree.mli
index b00827716..3718114a0 100644
--- a/helm/software/components/ng_refiner/nDiscriminationTree.mli
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.mli
@@ -24,7 +24,7 @@
  *)
 
 module NCicIndexable : Discrimination_tree.Indexable
-with type input = NCic.term and type constant_name = NUri.uri
+with type input = NCic.term and type constant_name = NReference.reference
 
 module TermSet : Set.S with type elt = NCic.term