The Coq mailing list

[t x <txrev319 AT gmail.com>]

Why is it that in

(1) Hint Extern 1 (?a = ?b) => idtac : mydb.

(2) Hint Extern 1 (?a) => idtac : mydb.

(1) is valid but (2) gets Error: bound head variable ?

In particular, I want a hint that matches on _all_ goals. This is so that I can do:

Hint Extern # _ =>

  match goal on

  | H1: ...,

    H2: ...

  end

to be able to match on hypothesis.

How do I make this work?

Thanks!