- let src_uri = CoercDb.coerc_carr_of_term src 0 in
- let tgt_uri = CoercDb.coerc_carr_of_term tgt 0 in
- look_for_coercion' metasenv subst context src_uri tgt_uri
+ let src_arity = count_pi context subst src in
+ let tgt_arity = count_pi context subst tgt in
+ let src_carr = CoercDb.coerc_carr_of_term src src_arity in
+ let tgt_carr = CoercDb.coerc_carr_of_term tgt tgt_arity in
+ look_for_coercion_carr metasenv subst context src_carr tgt_carr