let cache_empty = (Universe.empty,[]);;
let get_candidates (univ,_) ty =
let cache_empty = (Universe.empty,[]);;
let get_candidates (univ,_) ty =
assert false (* if succed it can't fail *)
;;
let cache_add_success ((univ,_) as cache) cache_key proof =
assert false (* if succed it can't fail *)
;;
let cache_add_success ((univ,_) as cache) cache_key proof =
(match cache_examine cache cache_key with
| Failed_in _ -> cache_replace cache cache_key (Succeded proof)
| UnderInspection -> cache_replace cache cache_key (Succeded proof)
(match cache_examine cache cache_key with
| Failed_in _ -> cache_replace cache cache_key (Succeded proof)
| UnderInspection -> cache_replace cache cache_key (Succeded proof)