The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Ralf, John,

isn't the problem of John that he can't instantiate the evar in the context 
of the current goal? It was stated before that an evar can be unified with 
any term of the same type. But this might not work in practice, because the 
resulting term might not be well typed in the context, in which the evar was 
created.

John suggested to focus on the evar itself as goal, because then obviously 
one would be in the right context to construct a well typed term for the 
evar. Are there other methods? If not, how can one focus an unnamed evar?

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928