From 8d6963c2cd6273fe60733ba3094e9567a17e5c51 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 4 Mar 2010 08:27:05 +0000 Subject: [PATCH] In line with the ml. --- helm/software/components/ng_refiner/nDiscriminationTree.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2