| C.LetIn (n,s,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
+ | 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')