let _ = sort_of_prod (sort1,sort2) in
C.Prod (n,s,type2)
| C.LetIn (n,s,t) ->
- let type1 = type_of_aux env s in
- let type2 = type_of_aux (type1::env) t in
- type2
+ let t' = CicSubstitution.subst s t in
+ type_of_aux env t'
| C.Appl (he::tl) when List.length tl > 0 ->
let hetype = type_of_aux env he
and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in