The Coq mailing list

[Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>]

You need a "dependent case" (the type of the result
depends on the matched value).

Inductive Vec : nat -> Set :=
              nil : (Vec O)
            | cons :(n:nat)(a:nat)(l:(Vec n))(Vec (S n)).

Variable c :nat.

Fixpoint vec_scale [n:nat;v:(Vec n)] : (Vec n) :=
         <[x](Vec x)>Cases v of
         | nil => nil
         | (cons m a l) => (cons m (mult a c) (vec_scale m l))
         end.

Jean-Francois