The Coq mailing list

[Lo�c Pottier <Loic.Pottier AT sophia.inria.fr>]

Hello,

 

is there a way to keep the name of bound variables when an hypothesis is eliminated?

 

For example:

 

 

Coq < Goal (exists eta:nat, eta=eta)-> True.
1 subgoal
 
  ============================
   (exists eta : nat, eta = eta) -> True

 

Unnamed_thm < intro.
1 subgoal
 
  H : exists eta : nat, eta = eta
  ============================
   True

 

Unnamed_thm < destruct H.
1 subgoal
 
  x : nat
  H : x = x
  ============================
   True

 

Unnamed_thm < 

 

Of course, I need a general mechanism, not an ad hoc solution, like:

 

generalize H; intro (eta,H1).

 

Loïc