X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoCache.ml;h=5fb4640d71e2c8308280a64e090c0bb5a32d6494;hb=3f676ab6acafa32514a44bc84d287f44dbc5389e;hp=57701310c445b3de47adc3e56aa3806708e397fc;hpb=cee1c02ad6a113b711b9d93176296cf16b9ec351;p=helm.git

diff --git a/helm/software/components/tactics/autoCache.ml b/helm/software/components/tactics/autoCache.ml
index 57701310c..5fb4640d7 100644
--- a/helm/software/components/tactics/autoCache.ml
+++ b/helm/software/components/tactics/autoCache.ml
@@ -35,7 +35,10 @@ type cache = (Universe.universe * ((cache_key * cache_elem) list));;
 let cache_empty = (Universe.empty,[]);;
 
 let get_candidates (univ,_) ty = 
-  Universe.get_candidates univ ty
+  if Universe.key ty = ty then
+    Universe.get_candidates univ ty
+  else 
+    []
 ;;
 
 let index (univ,cache) key term =
@@ -77,7 +80,10 @@ let cache_add_failure cache cache_key depth =
       assert false (* if succed it can't fail *)
 ;;
 let cache_add_success ((univ,_) as cache) cache_key proof =
-  Universe.index univ cache_key proof,snd
+  (if Universe.key cache_key = cache_key then
+    Universe.index univ cache_key proof
+  else
+    univ),snd
   (match cache_examine cache cache_key with
   | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
   | UnderInspection -> cache_replace cache cache_key (Succeded proof)