The Coq mailing list

[Arthur Chargu�raud<arthur.chargueraud AT inria.fr>]

The trick I use is to perform an anonymous intro, 
then use "match" to obtain the name of the most-recently
introduced hypothesis, and then revert this hypothesis.
On the way, I'm able to access the name that used to
be bound in the goal. Here is the demo script:


Ltac get_last_name := 
  match goal with x:_ |- _ => x end.

Lemma test : forall a:nat, a = a.
  intro; let x := get_last_name in revert x; 
  let x2 := fresh x "2" in idtac x2.
  (* displays a2 *)


Arthur