From d0e058e37a75dcb0247b0b0efbe99e68ce1ceca4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 26 May 2008 13:58:13 +0000 Subject: [PATCH] Universe.key was not used to index terms, but was used to retrieve them --- helm/software/components/tactics/autoCache.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/helm/software/components/tactics/autoCache.ml b/helm/software/components/tactics/autoCache.ml index b12b26c05..7458e5777 100644 --- 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 ;; -- 2.39.2