The Coq mailing list

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

 

Hi,

 I have a goal

 

H: ex_T R (fun eta:R => P eta)

======================

...

 

with

 

elim H; intros

 

the name of the existemtial variable eta is forgotten and replaced with x!

 

How to keep trace of this name and obtain a goal:

 

eta:R

H0: P eta

==========================

...

 

???

 

Loïc