The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/23/2014 10:29 AM, Jason Gross wrote:
> If you have your hands on an evar in Ltac, is there a way to get it as a
> goal?  For example, could I do something like:
>
> match type of H with
>    | _ /\ ?R => is_evar R; R: refine (_ : _ /\ _)
> end

That doesn't work for me at all - why not ...=> is_evar R; assert R?

Also, this doesn't answer my question of how to deal with evars buried 
deep inside of complex terms.

-- Jonathan