The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

IMO, this is a great illustration of why Coq should never infer 
dependent-match annotations, except in copying down the type of the 
current function verbatim.

On 04/07/2014 06:28 AM, Ömer Sinan Ağacan wrote:
> This is weird. Coq was saying that the problem is with cons branch,
> not nil branch. But when I changed nil branch it worked. So this also
> works:
>
> Fixpoint pt_aux h len (v : Vector.t nat len) : Vector.t nat len :=
>    match v with
>    | Vector.nil =>  Vector.nil nat
>    | Vector.cons h' _ t' =>
>        Vector.cons nat (h + h') _ (pt_aux h' _ t')
>    end.
>
> Thanks again.
>