From: Enrico Tassi Date: Tue, 2 Mar 2010 11:53:57 +0000 (+0000) Subject: Constants are indexed using the Reference, not the Uri, so that constructors X-Git-Tag: make_still_working~3022 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2b52dcc1742d2ee0616b6526e3ade1dd21ec10f3;p=helm.git 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 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 ;;