Universe.key was not used to index terms, but was used to retrieve them

diff --git a/helm/software/components/tactics/autoCache.ml b/helm/software/components/tactics/autoCache.ml
index b12b26c054853d8288ddbc68d7e5e9dd93927c34..7458e577748bd99e731f9592bbdeebceac534e80 100644 (file)
--- a/helm/software/components/tactics/autoCache.ml
+++ b/helm/software/components/tactics/autoCache.ml
@@ -39,10 +39,12 @@ let prerr_endline s =
 let cache_empty = (Universe.empty,[]);;
 
 let get_candidates (univ,_) ty = 
-  if Universe.key ty = ty then
+(*   if Universe.key ty = ty then *)
     Universe.get_candidates univ ty
+(*
   else 
-    []
+    (prerr_endline ("skip: " ^ CicPp.ppterm (Universe.key ty)); [])
+ *)
 ;;
 
 let index (univ,cache) key term =
@@ -57,6 +59,7 @@ let cache_add_list (univ,cache) context terms_and_types =
   let univ = 
     List.fold_left
       (fun univ (t,ty) -> 
+         prerr_endline ("indexing: " ^ CicPp.ppterm ty);
         Universe.index_local_term univ context t ty)
       univ terms_and_types  
   in
@@ -64,7 +67,8 @@ let cache_add_list (univ,cache) context terms_and_types =
 
 let cache_examine (_,oldcache) cache_key = 
   prerr_endline ("examine : " ^ CicPp.ppterm cache_key);
-  try List.assoc cache_key oldcache with Not_found -> 
+  try snd (List.find (fun (x,_) -> CicUtil.alpha_equivalence x cache_key) 
+        oldcache) with Not_found -> 
     prerr_endline "notfound";
     Notfound
 ;;