The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Hi,

  I'm trying to use ltac to match vs a "forall"

## Context

== BEGIN ==

Ltac get_tail_valid H :=

  match H with

  | forall _, ?H' => get_tail_valid H'

  end.

Ltac get_tail_fail2 H :=

  match H with

  | forall ?x:?T, ?H' => get_tail_fail2 H'

  end.

Ltac get_tail_fail1 H :=

  match H with

  | forall ?x, ?H' => get_tail_fail1 H'

  end.

== END ==

  Here's the interesting thing.

  (1) If I don't try to capture the forall varaible -- if I use "_", it compiles.

  (2) If I try to capture the forall varaible (i.e. either as "?x:?T" or "?x"), Coq does not compile.

## Question

  1) What am I doing wrong?

  2) How do I "capture" the forall variable?

Thanks!