- inside dicrimination_tree is now checked the invariant that bad terms are indexed...

[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 57701310c445b3de47adc3e56aa3806708e397fc..5fb4640d71e2c8308280a64e090c0bb5a32d6494 100644 (file)
--- 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)