Remove warning about size mismatch in pretyping
Remove warning about size mismatch in pretyping

It is considered not useful enough. We rely instead on the tests in
typing, where we know the exact lengths of arrays.

jasmin-lang/jasmin,jasmin-lang/jasmin,jasmin-lang/jasmin