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)
- | C.Appl l ->
- let l' = List.map (eta_fix' context) l
- in
- (match l' with
- [] -> assert false
- | he::tl ->
- let ty,_ =
- CicTypeChecker.type_of_aux' metasenv context he
- CicUniv.empty_ugraph
- in
- fix_according_to_type ty he tl
+ (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
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context he
+ CicUniv.empty_ugraph
+ in
+ fix_according_to_type ty (eta_fix' context he) tl'
(*
C.Const(uri,exp_named_subst)::l'' ->
let constant_type =
) in
fix_according_to_type
constant_type (C.Const(uri,exp_named_subst)) l''
- | _ -> C.Appl l' *))
+ | _ -> C.Appl l' *)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
C.Const (uri,exp_named_subst')