| C.Sort _ as t -> t (* l should be empty *)
| C.Implicit _ as t -> t
| C.Cast (te,ty) ->
- C.Cast (reduceaux context l te, reduceaux context l ty)
+ C.Cast (reduceaux context l te, reduceaux context [] ty)
| C.Prod (name,s,t) ->
assert (l = []) ;
C.Prod (name,