coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] unshelve

From: Simon Boulier <simon.boulier AT ens-rennes.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] unshelve
Date: Thu, 30 Jun 2016 15:56:56 +0200

Hi Coq-Club,

Thanks to Pierre-Marie Pédrot I discovered an new fancy undocumented tactic!

"unshelve tac" do the tactic "tac" and then unshelve the generated evars.

I find "unshelve econstructor" and "unshelve eapply foo" very useful...

Enjoy!

Simon

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] unshelve, Simon Boulier, 06/30/2016