let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
match infty, expty with
| (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
match infty, expty with
| (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),