?depth:int ->
?width:int ->
?timeout:float ->
- ?auto:Equality_retrieval.auto_type ->
+ Equality_retrieval.auto_type option ->
ProofEngineTypes.status ->
ProofEngineTypes.proof * ProofEngineTypes.goal list
HMysql.dbd ->
ProofEngineTypes.status ->
bool -> (* smart_flag *)
- ?auto:Equality_retrieval.auto_type ->
- AutoCache.cache ->
+ Equality_retrieval.auto_type option ->
+ AutoCache.cache ->
Equality.equality_bag *
Equality.equality list * AutoCache.cache * int
-val saturate_more:
+
+val close_more:
Equality.equality_bag ->
active_table ->
int -> (* maxmeta *)
ProofEngineTypes.status ->
bool -> (* smart flag *)
- ?auto:Equality_retrieval.auto_type ->
+ Equality_retrieval.auto_type option ->
AutoCache.cache ->
Equality.equality_bag * Equality.equality list * AutoCache.cache * int