The Coq mailing list

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

I was working through CPDT, the Match chapter, and created an Ltac to pose a list of vals based off of the "Ltac length" function therein:

--------------------------------------------------------------------------
Ltac poseList ls :=
  match ls with
    | nil => idtac
    | ?i :: ?ls' => pose i ; poseList ls'
  end.

Goal True .

  poseList (1 :: 2 :: 3 :: nil) .

  Abort.
--------------------------------------------------------------------------

The above works as expected, adding n, n0 and n1 to the hyopthesis.

When I try to use:

-------------------------------------------------------------------------
Definition vals := (1 :: 2 :: 3 :: nil) .

Goal True .

  poseList vals .

  Abort.
--------------------------------------------------------------------------

I get an error:

  No matching clauses for match

Am I approaching this the wrong way, or am I missing some bit of syntax to make it work?

I also tried using:
 
--------------------------------------------------------------------------

Goal True.

  pose vals.

  match goal with

    | [ H : (_ : list nat) |- _ ] =>
      let v' := eval unfold H in H in
      poseList v'
  end .

--------------------------------------------------------------------------

to try to unwrap the vals, but it fails with a similar error.
  No matching clauses for match goal

Thanks,

Mike Kaplan