+ 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))
+(*