| C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
| C.Implicit -> raise (Impossible 21)
| C.Cast (te,ty) ->
- let _ = type_of ty in
+ let _ = type_of_aux context ty in
if R.are_convertible (type_of_aux context te) ty then ty
else raise (NotWellTyped "Cast")
| C.Prod (_,s,t) ->