The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

Consider the following block of code:

== BEGIN ==

Ltac simp_rem v :=

  let nV := fresh "var_" in

  let nH := fresh "H_eq_var_" in

    remember v as nV eqn: nH.

Lemma lem_000:

  forall (a : nat), (a+2) = 2.

Proof.

  intro a.

  simp_rem (a+2).

  Abort.

== END ==

The output I get is:

1 subgoal

a : nat

var_ : nat

nH : var_ = a + 2

====================================================================== (1/1)

var_ = 2

I like the fact that the newly introduced var has prefix "var_"

I don't like the fact that the equation is named nH instead of something with prefix "H_eq_var_"

It is important to me that (1) I don't clash with existing hypothesis names and (2) I know the name of the newly introduced equation so that I can apply other transforms to it.

Question:

1) What am I doing wrong?

2) How do I fix this?

Attachment: fail.v
Description: Binary data