+ let (_,recindex,_,body) = List.nth fl i in
+ let recparam =
+ try
+ Some (List.nth l recindex)
+ with
+ _ -> None
+ in
+ (match recparam with
+ Some recparam ->
+ (match reduceaux context [] recparam with
+ C.MutConstruct _
+ | C.Appl ((C.MutConstruct _)::_) ->
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
+ fl
+ body
+ in
+ (* Possible optimization: substituting whd recparam in l*)
+ reduceaux context l body'
+ | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
+ )
+ | None -> if l = [] then t' () else C.Appl ((t' ())::l)
+ )
+ | C.CoFix (i,fl) ->
+ let tys =
+ List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+ in
+ let t' =
+ let fl' =
+ List.map
+ (function (n,ty,bo) ->
+ (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
+ ) fl
+ in