The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> 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?

John was asking about something like `only [n]: refine (S _)` for unnamed 
evars,
and the answer is `instantiate (1 := ltac:(refine (S _)))`.
Admittedly, that's still not focusing in the sense of actually bringing the
context on the screen in CoqIDE/ProofGeneral.  I don't know how to do that 
even
for named evars...

Kind regards,
Ralf

> 
> 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
>