X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FautoCache.ml;h=5fb4640d71e2c8308280a64e090c0bb5a32d6494;hb=cfbcef4637ff26ac4dfefe41bf2df29222e80138;hp=57701310c445b3de47adc3e56aa3806708e397fc;hpb=06b128f1107fd579a696b83b2f8255f83ab29a92;p=helm.git

diff --git a/components/tactics/autoCache.ml b/components/tactics/autoCache.ml
index 57701310c..5fb4640d7 100644
--- a/components/tactics/autoCache.ml
+++ b/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)