-type universe
-val empty_universe:universe
-val get_candidates: universe -> Cic.term -> Cic.term list
-val universe_of_goals:
- HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list ->
- universe -> universe
-val universe_of_context: Cic.context -> Cic.metasenv -> universe -> universe
-
-type cache
-type cache_key = Cic.term
-type cache_elem =
- | Failed_in of int
- | Succeded of Cic.term
- | UnderInspection
- | Notfound
-val cache_examine: cache -> cache_key -> cache_elem
-val cache_add_failure: cache -> cache_key -> int -> cache
-val cache_add_success: cache -> cache_key -> Cic.term -> cache
-val cache_add_underinspection: cache -> cache_key -> int -> cache
-val cache_empty: cache
-