(* $Id$ *)
+
val saturate :
HMysql.dbd ->
?full:bool ->
?width:int ->
ProofEngineTypes.proof * ProofEngineTypes.goal ->
(UriManager.uri option * Cic.conjecture list * Cic.term * Cic.term) *
- 'a list
+ ProofEngineTypes.goal list
val weight_age_ratio : int ref
val weight_age_counter: int ref