coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Dependent Subgoals in Coq 8.4
- Date: Sun, 10 Apr 2016 22:19:57 -0400
- 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-oi0-f52.google.com
- Ironport-phdr: 9a23:36968h/NcLSXfv9uRHKM819IXTAuvvDOBiVQ1KB91+McTK2v8tzYMVDF4r011RmSDdWdt6IP0bOI+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt6U05T8jbnss7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR/QMBzM/dmsx+cfDtB/ZTALJ6GFKAUsMlR8dIQHe6xeycY32qTCy4uh0wy6cMtfxVqtlcTun5qZvDhTvjXFUZHYC7GjLh5ko3+pgqxW7qkknzg==
I discovered just now that Coq 8.4 supports dependent subgoals, if a bit awkwardly. In the following, solving the second goal instantiates an evar in the first goal:
Goal True.
eapply (let x := _ in _).
Grab Existential Variables.
Was this known? Was this supported? (I know that the ssreflect plugin gave limited support for dependent subgoals in 8.4...)
-Jason
- [Coq-Club] Dependent Subgoals in Coq 8.4, Jason Gross, 04/11/2016
Archive powered by MHonArc 2.6.18.