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