The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/26/2016 02:13 PM, Jason Gross wrote:
> Right, I think I do need the setup.  I was mainly wondering if I could get
> rid of the Unshelve.  I think I saw a comment by you on some bug report
> mentioning that instantiate works with named evars?  That seems like it'd
> be enough to wrap the whole thing up into pre_show_goal, show_goal, and
> post_show_goal tactics, with no vernacular needed.

Oh, so you want the "observer" goal to remain hidden after the setup, 
but to be recoverable later, correct?  So you are trying to make the 
observer goal be a named evar, so that it is recoverable later by name?  
Here is an Ltac hack that can do that:

Variable F : Type.
Goal F.
(*setup and shelve observer with evar name __Observer*)
lazymatch goal with
|- ?G => simple refine (let x := _ : G in ?[__Observer]); [|shelve]
end.
(*evolution of observed goal*)
pose (x:=1).
destruct x.
(*recovery of observer*)
unshelve instantiate (__Observer := _).

Warning: this type of Ltac hackery is bound to incur the ire of the 
devs.  Use at your own risk.

-- Jonathan