+ let rec count_prods context ty =
+ match CicReduction.whd context ~subst:subst'' ty with
+ | Cic.Prod (n,s,t) ->
+ 1 + count_prods (Some (n,Cic.Decl s)::context) t
+ | _ -> 0
+ in
+ let exp_prods = count_prods context ty' in
+ let inf_prods = count_prods context inferredty in
+ let te', inferredty, metasenv'', subst'', ugraph2 =
+ let rec aux t m s ug it = function
+ | 0 -> t,it,m,s,ug
+ | n ->
+ match CicReduction.whd context ~subst:s it with
+ | Cic.Prod (_,src,tgt) ->
+ let newmeta, metaty, s, m, ug =
+ type_of_aux s m context (Cic.Implicit None) ug
+ in
+ let s,m,ug =
+ fo_unif_subst s context m metaty src ug
+ in
+ let t =
+ match t with
+ | Cic.Appl l -> Cic.Appl (l @ [newmeta])
+ | _ -> Cic.Appl [t;newmeta]
+ in
+ aux t m s ug (CicSubstitution.subst newmeta tgt) (n-1)
+ | _ -> t,it,m,s,ug
+ in
+ aux te' metasenv'' subst'' ugraph2 inferredty
+ (max 0 (inf_prods - exp_prods))
+ in