(* given he:hety, gives beack all (c he) such that (c e):?->? *)
let fix_arity n metasenv context subst he hetype ugraph =
let hetype = CicMetaSubst.apply_subst subst hetype in
- let src = CoercDb.coerc_carr_of_term hetype 0 in
- let tgt = CoercDb.coerc_carr_of_term (Cic.Implicit None) 1 in
- match CoercGraph.look_for_coercion' metasenv subst context src tgt with
+ (* instead of a dummy functional type we may create the real product
+ * using args_bo_and_ty, but since coercions lookup ignores the
+ * actual ariety we opt for the simple solution *)
+ let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
+ match CoercGraph.look_for_coercion metasenv subst context hetype fty with
| CoercGraph.NoCoercion -> []
| CoercGraph.NotHandled ->
raise (MoreArgsThanExpected (n,Uncertain (lazy "")))