- (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.oblivion_ugraph
+ in
+ fix_according_to_type ty (eta_fix' context he) tl'