+let prerr_endline _ = ();;
+
+(*
+let rec fix_lambdas_wrt_type ty te =
+ let module C = Cic in
+ let module S = CicSubstitution in
+(* prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
+ match ty with
+ C.Prod (_,_,ty') ->
+ (match CicReduction.whd [] te with
+ C.Lambda (n,s,te') ->
+ C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
+ | t ->
+ let rec get_sources =
+ function
+ C.Prod (_,s,ty) -> s::(get_sources ty)
+ | _ -> [] in
+ let sources = get_sources ty in
+ let no_sources = List.length sources in
+ let rec mk_rels n shift =
+ if n = 0 then []
+ else (C.Rel (n + shift))::(mk_rels (n - 1) shift) in
+ let t' = S.lift no_sources t in
+ let t2 =
+ match t' with
+ C.Appl l ->
+ C.LetIn
+ (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
+ | _ ->
+ C.Appl (t'::(mk_rels no_sources 0)) in
+ List.fold_right
+ (fun source t -> C.Lambda (C.Name "y",source,t))
+ sources t2)
+ | _ -> te
+;; *)
+
+let rec fix_lambdas_wrt_type ty te =
+ let module C = Cic in
+ let module S = CicSubstitution in
+(* prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
+ match ty,te with
+ C.Prod (_,_,ty'), C.Lambda (n,s,te') ->
+ C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
+ | C.Prod (_,s,ty'), t ->
+ let rec get_sources =
+ function
+ C.Prod (_,s,ty) -> s::(get_sources ty)
+ | _ -> [] in
+ let sources = get_sources ty in
+ let no_sources = List.length sources in
+ let rec mk_rels n shift =
+ if n = 0 then []
+ else (C.Rel (n + shift))::(mk_rels (n - 1) shift) in
+ let t' = S.lift no_sources t in
+ let t2 =
+ match t' with
+ C.Appl l ->
+ C.LetIn (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
+ | _ -> C.Appl (t'::(mk_rels no_sources 0)) in
+ List.fold_right
+ (fun source t -> C.Lambda (C.Name "y",CicReduction.whd [] source,t)) sources t2
+ | _, _ -> te
+;;
+
+(*