- match infty, expty with
- | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) ->
- let module CS = CicSubstitution in
+ match infty, expty, t with
+ | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) ->
+ (match fl with
+ [name,i,_(* infty *),bo] ->
+ let context_bo =
+ Some (Cic.Name name,Cic.Decl expty)::context in
+ let (rel1, _), subst, metasenv, ugraph =
+ coerce_to_something_aux (Cic.Rel 1) expty infty subst
+ metasenv context_bo ugraph in
+ let bo =
+ CS.subst ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 bo)
+ in
+ let (bo,_), subst, metasenv, ugraph =
+ coerce_to_something_aux bo infty expty subst
+ metasenv context_bo ugraph
+ in
+ (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
+ | _ -> assert false (* not implemented yet *)
+ )
+ | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->