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