The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

You first need to skolemize x before doing that unification, so that it 
has no hyps.  You can also then set up the new goal with no hyps as well 
- so they will then both have no hyps at the point of the unification.

To skolemize, do something like "instantiate (1 := ltac:(revert_all))", 
where revert_all is the obvious:

Ltac revert_all := repeat lazymatch goal with H : _ |- _ => revert H end.

-- Jonathan


On 04/01/2017 02:20 PM, Jason Gross wrote:
> Say I have an Ltac variable x such that [is_evar x] succeeds.  How do I get
> a goal corresponding to x, in an Ltac script (without vernaculars)?  I
> tried making a new goal and unifying the evar of that goal with x, but that
> fails with a "not well typed in the context of x" message, because I have
> different hypotheses.
>
> Thanks,
> Jason