The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

Yves Bertot wrote:
> That's a nice suggestion.  One could have a "Extential to goal" 
> command.

So it would not be possible to automate using this feature by Ltac? (That
seems a shame)

Sam wrote:
> So, for example, one might write:
>     refine (f (exist _ x #) #).

Often I find that:
  refine (let u1 := _ in let u2 := _ in f (exist _ x u1) u2).
works, but I don't know if it suits every situation.



-- 
View this message in context: 
http://www.nabble.com/Instantiating-existential-variables-tp22390035p22479143.html
Sent from the Coq mailing list archive at Nabble.com.