The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Adam Chlipala 
<adamc AT csail.mit.edu>
 writes:

> In my opinion, it is a very handy feature to make out-of-the-box
> vectors difficult to work with, since almost no one should be using
> dependently typed vectors for anything.

What should then the proper alternative recommended alternative for
sized lists in the standard library?

E.