val find_context_equalities:
int -> (* maxmeta *)
Equality.equality_bag ->
- ?auto:auto_type ->
+ auto_type option ->
Cic.context -> ProofEngineTypes.proof -> (* FIXME:Why bot context and proof?*)
AutoCache.cache ->
int list * Equality.equality list * int * AutoCache.cache
*)
val find_library_equalities:
Equality.equality_bag ->
- ?auto:auto_type ->
+ auto_type option->
bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
AutoCache.cache ->
UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int *