The Coq mailing list

[Frederic Blanqui <blanqui AT loria.fr>]

On Tue, 13 Mar 2007, 
roconnor AT theorem.ca
 wrote:

> Many people complain that using Vectors is difficult.  It is true if you are 
> doing things like concatinating lists.  For my purposes they worked fine

it is not so difficult to use thanks to the implicit arguments mechanism. most 
of the time, coq infers itself the necessary indices.