From dc02fa875548541fd9ca33ec8f191a4fc149588f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 22 Apr 2008 12:50:33 +0000 Subject: [PATCH 1/1] fix cache comparison relaxed to URI and not REFERENCE --- helm/software/components/ng_kernel/oCic2NCic.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 4aaeb414c..8298e65e3 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -281,8 +281,13 @@ let alpha t1 t2 ref ref' = | NCic.Prod (_,s1,t1), NCic.Prod (_,s2,t2) -> aux s1 s2; aux t1 t2 | NCic.LetIn (_,s1,ty1,t1), NCic.LetIn (_,s2,ty2,t2) -> aux s1 s2; aux ty1 ty2; aux t1 t2 - | NCic.Const r1, - NCic.Const r2 when NReference.eq r1 ref && NReference.eq r2 ref' -> () + | NCic.Const (NReference.Ref (_,uu1,_)), + NCic.Const (NReference.Ref (_,uu2,_)) when + let NReference.Ref (_,u1,_) = ref in + let NReference.Ref (_,u2,_) = ref' in + (uu1 == u1 && uu2 == u2) || + (uu1 == u2 && uu2 == u1) + -> () | NCic.Const r1, NCic.Const r2 when NReference.eq r1 r2 -> () | NCic.Meta _,NCic.Meta _ -> () | NCic.Implicit _,NCic.Implicit _ -> () @@ -321,15 +326,13 @@ let find_in_cache name obj ref = prerr_endline ("!!!!!!!!!!! CACHE HIT !!!!!!!!!!\n" ^ NReference.string_of_reference ref ^ "\n" ^ NReference.string_of_reference ref' ^ "\n"); -*) + *) raise (Found ref')); - (* prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==> " ^ NReference.string_of_reference ref'); -*) - + *) ) (Hashtbl.find_all cache name); -(* prerr_endline "<<< CACHE MISS >>>"; *) +(* prerr_endline "<<< CACHE MISS >>>"; *) begin match obj, ref with | (_,_,_,_,NCic.Fixpoint (true,fl,_)) , NReference.Ref (x,y,NReference.Fix _) -> -- 2.39.2