The Coq mailing list

[Mike Kaplan <michael.n.kaplan AT gmail.com>]

Thanks, that's exactly what I was looking for. 

On Tue, Sep 24, 2013 at 11:24 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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