- let eq_uri = eq_of_goal ty in
- let bag = Equality.mk_equality_bag () in
- let eq_indexes, equalities, maxm, cache =
- Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty
- in
- let lib_eq_uris, library_equalities, maxm, cache =
- Equality_retrieval.find_library_equalities bag None
- false dbd context (proof, goal) (maxm+2) cache
- in
- if library_equalities = [] then prerr_endline "VUOTA!!!";