coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] shelf

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] shelf
Date: Mon, 12 Aug 2019 09:54:07 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f45.google.com
Ironport-phdr: 9a23:TYg9DRD801M3R1IPkEBCUyQJP3N1i/DPJgcQr6AfoPdwSPv/pcbcNUDSrc9gkEXOFd2Cra4d0ayP6furADZdqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmssAndqMcbjYR/JqovyhbCv2dFdflRyW50P1yYggzy5t23/J5t8iRQv+wu+stdWqjkfKo2UKJVAi0+P286+MPkux/DTRCS5nQHSWUZjgBIAwne4x7kWJr6rzb3ufB82CmeOs32UKw0VDG/5KplVBPklCEKPCM//WrKiMJ/kbhbrQquqBxxwYHaYI+bOvljcK3DYdwXXnBOUtpLWiFbHo+wc4kCAuwcNuhYtYn9oF4OoAOkCwmtGuzv0CVIiWHr1qAk1OQhDBvG3BAhH90QrXTfsdL4NL8TUe+r1qnI1yvMY+lK1jf69YjIaAwhofCSUrJtasfRxkwvGBnEjlWUs4DqIzSV1uEUvmWd8uFuVvqvhnY5pw1tpjWj3MQhh4nTio4L11zI6T91zYk1KNC+VUV1e8SrEIFKuCGfL4Z2Qt0tQ2VvuCsiz70Jo5+7fCwTxJQg2x7TduWLc4aH7x/jTuqRLjB4hHVqeLK7mRm+61Svyur5VsWs0VZKqDRKksXUu3wTyxDe7tKLR/h980u7xzqDyhzf5vtLLE00jabbLoQuwr80lpodq0TDGSr2lV3ujK+XaEok4PKo5Pr9brr6oZ+cKpV0ih3/Mqswh8yyGus4Mg0UUGia/eSwzqHs/Ur8QLlSlP05jrHZsIzGJcQcvqO2HwhV0p865xmjCzemzc8XkGIcLFNFfRKHl5LmN0vPIPD+F/e/gk6jnC1lx/DcbfXdBcDGKWGGm7P8d5587VRdwUw914Nx/ZVRX4kALejpVwfas8HCEh40LkTg2+fqEs9wkIgZRHiTA6KEGKzXuF6MoOkoJr/fN8cupD/hJq19tLbVhngjlApFJPT77d4scHm9W89eDQCZbH7r2IpTFG4Luk85ULWvhgHfFzFUYHm2UuQ34TRpUNv6X7eGfZikhfm65An+BodfPzkUBVWFEHOufIKBCa9VOXCiZ/R5mzlBboCPDooo1BWgrgj/kuM1Ie/d+ylevpXmhoF4

The shelf contains goals that coq believes will be solved by unification. It is rather accurate until you play with existential variables (eapply etc).

Hope this helps

Pierre

Le lun. 12 août 2019 à 09:23, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :

Hi,

I have the message
All the remaining goals are on the shelf.

In the documentation index there is a pointer to tactics shelve (etc)
which in turn gives a pointer to a command Unshelve, which seems to
enable me to continue my proof.

However I can't find anything about what is the shelf, and why some
goals sometimes go there.

Thanks

Jeremy

[Coq-Club] shelf, Jeremy Dawson, 08/12/2019
- Re: [Coq-Club] shelf, Pierre Courtieu, 08/12/2019