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.LetIn (C.Name "w",t',assert false,
+ 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
(* prerr_endline ("******* too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *)
C.LetIn
(C.Name "H",
- C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
+ C.Appl res,
+ assert false,
+ C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
else
let name,source,target =
(match ty with
| C.Lambda (n,s,t) ->
C.Lambda
(n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
C.LetIn
- (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
+ (n,eta_fix' context s,eta_fix' context ty,
+ eta_fix' ((Some (n,(C.Def (s,ty))))::context) t)
| C.Appl [] -> assert false
| C.Appl (he::tl) ->
let tl' = List.map (eta_fix' context) tl in