- Universe.index univ cache_key proof,snd
- (match cache_examine cache cache_key with
+ let u_key = Universe.key cache_key in
+ if u_key <> cache_key then
+ Universe.index univ u_key proof, snd cache
+ 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)
+ | Succeded t -> (* we may decide to keep the smallest proof *) cache
+ | Notfound -> cache_replace cache cache_key (Succeded proof))
+(*
+ (if Universe.key cache_key = cache_key then
+ Universe.index univ cache_key proof
+ else
+ univ),snd
+ (prerr_endline ("CACHE: ADD SUCCESS" ^ CicPp.ppterm cache_key);
+ match cache_examine cache cache_key with