fix cache comparison relaxed to URI and not REFERENCE

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 4aaeb414c4d8330e70b6dc4cd3d224981b254f66..8298e65e3b4c14faa875a3fe6abb606ef789eb6e 100644 (file)
--- 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 _) ->