parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / autoCache.ml

diff --git a/helm/software/components/tactics/autoCache.ml b/helm/software/components/tactics/autoCache.ml
index b12b26c054853d8288ddbc68d7e5e9dd93927c34..882a1839309ff21a2cc5ee5284aaf33082deb329 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
 ;;
@@ -149,3 +153,6 @@ let cache_size (_,oldcache) =
 let cache_clean (univ,oldcache) = 
   univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache
 ;;
+let cache_reset_underinspection (u,c) =
+  u,List.filter (function (_,UnderInspection) -> false | _ -> true) c
+;;