From 2b52dcc1742d2ee0616b6526e3ade1dd21ec10f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 2 Mar 2010 11:53:57 +0000 Subject: [PATCH] Constants are indexed using the Reference, not the Uri, so that constructors are different! --- .../components/ng_refiner/nDiscriminationTree.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml index fff8b6769..2bae037c1 100644 --- 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 ;; -- 2.39.2