;;
(* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion' metasenv subst context src tgt =
+let look_for_coercion_carr metasenv subst context src tgt =
let is_dead = function CoercDb.Dead -> true | _ -> false in
let pp_l s l =
match l with
| ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
;;
+let rec count_pi c s t =
+ match CicReduction.whd ~delta:false ~subst:s c t with
+ | Cic.Prod (_,_,t) -> 1 + count_pi c s t
+ | _ -> 0
+;;
+
let look_for_coercion metasenv subst context src tgt =
- 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
let source_of t =
match CoercDb.is_a_coercion t with