The Coq mailing list

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

On 09/24/2013 11:10 AM, Mike Kaplan wrote:
> --------------------------------------------------------------------------
> Ltac poseList ls :=
>   match ls with
>     | nil => idtac
>     | ?i :: ?ls' => pose i ; poseList ls'
>   end.
>
> [...]
> --------------------------------------------------------------------------
>
> When I try to use:
>
> -------------------------------------------------------------------------
> Definition vals := (1 :: 2 :: 3 :: nil) .
> Goal True .
>   poseList vals .
>   Abort.
> --------------------------------------------------------------------------
>
> I get an error:

All this makes perfect sense, since Ltac matching is purely syntactic, 
and [vals] is neither [nil] nor a [cons]!

Many options are possible to do reduction in Ltac, and I do think CPDT 
introduces them at various points, but one option that would work here 
is replacing
    match ls with
with
    match eval hnf in ls with