coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] 8.4-compatible way of efficiently stripping unused evars?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] 8.4-compatible way of efficiently stripping unused evars?
Date: Thu, 29 Sep 2016 01:32:20 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f50.google.com
Ironport-phdr: 9a23:w74NpBWH0bRw5D1yMPikJEcmrc7V8LGtZVwlr6E/grcLSJyIuqrYZhCGt8tkgFKBZ4jH8fUM07OQ6PG6HzVQqsvY+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrr0os2YPlwArQH+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSRGAtNHlw78n2vzHCSxGO7z0SSDNFvABPBl3n5Qr9WN/eqCzhraIp2iCBOsv5V7cvQmWK4KJiSRuugyACYW1quFrLg9B92foI6CmqoAZyltbZ

Hi,

I'm working on a project that needs to build in both 8.4 and 8.5/8.6, so I can't use uconstr. Is there a way to "postprocess" an open_constr to drop all the associated evars from the proof, in a way that's compatible with 8.4? For example, can I do something to "foo" in "silly" in the code below to make the proof go through in both 8.4 and 8.6?

Tactic Notation "silly" open_constr(foo) := constructor.

Goal True.

silly _.

Qed.

Context: I want a way to not have to write the boilerplate of [fun T => match T with context[some pattern] => idtac end] a few dozen times, and instead just pass in the pattern. (I know that I could unify the type with itself with the open_constr plugged in to resolve the evars, but that seems expensive.)

Thanks,

Jason

[Coq-Club] 8.4-compatible way of efficiently stripping unused evars?, Jason Gross, 09/29/2016