The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Hi,

  1) In a previous question, I learned that I can do:

    destruct <expr> eqn:<naming intro pattern>

  2) To avoid the use of local variable names, I would like to wrap this in a ltac. However, I need to provide a name to "eqn: ... ".

Thus, my question -- what is the Coq equiv of gen-sym?

Thanks!