coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] shelf
- Date: Mon, 12 Aug 2019 07:22:46 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=8gDaWeBGefHNsF7jCxV3GnGb7umc0vygilnmrqWuRWU=; b=EdzLsxiH6UD15H7OqUqrHh34DsJd7OpNU2vIhK8n/DkhStakgO6gICpTRtzIxmSSoy38RxMPgL8D5H2JGu3xJH3BWRQhtD6FXRlWFZ0/HmS51Wox07KWlCMIS6Sa+UJKH/CC8t61dhAYacfr/EymRPdRCNFJUGq4benZ5TEw1DhauRo0EirIA0kptKVlDEHdUzjrvzOznalmFkBJnT3YXt7ylNNmhqjY0cCkCNudJpYyyrC9b8+tR9IIf/gF08GkNRRKw+zLAuooRaBxUovWEj0/PJNDHnKQGiYMcHzfF4CL9LZQ77yYFAuHFkCN2xWdPAqM2poO0nZ3XUtYfkvtoA==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=cDaaeIpEs1IbWP+YKjx8Jkyd8UcJ2sjDK9t7Qro6fTQKfDBVtte6sT8omB/t3tuu2qGtFkSS8/0X2H/tmUmG5vGIuqggwtD0wthlsRLWg98ychqrgoYTbZo2b9qzjLEVSxiIhA25TvZH9yPRNQkM3pQCibdgU8pcTlMoi7NMtaNUErP1yp34mUEl/KO96NSBk6gC21Wsfg4IohykowlAa+yiWsf7J7BKOmVyyGvWIHx0s+DeYcbmWRSVCOGf4WHA1TuZfCESv5wjLu45qmMqoZIIZP2GFLA/sdKsR4gm/D1jjkra//Q4PCsPSG5avebjyCSPYPGTPCH6mT40Sn/28g==
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:n+IrhBBVad33abWq1wlYUyQJP3N1i/DPJgcQr6AfoPdwSPTzoMbcNUDSrc9gkEXOFd2Cra4d0ayP6furADVQqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmssAndqMcbjYR/JqosyRbCv2dFdflRyW50P1yYggzy5t23/J5t8iRQv+wu+stdWqjkfKo2UKJVAi0+P286+MPkux/DTRCS5nQHSWUZjgBIAwne4x7kWJr6rzb3ufB82CmeOs32UKw0VDG/5KplVBPklCEKPCM//WrKiMJ/kbhbrQqhqRJh3oDUfI+bOvl/fqzBct0VSnFMXtpKWCFbHo+wc5cDAugHMO1Fr4f9vVwOrR6mCAeoGuzv0CFHhnr23KYn3eouCw/H3BcnH9IIrX/Zq9H7O7kIUe+ryanJzS/PYf1M1jbz84jIdRYhrOqWUrJ2bMrd01cgGB7YjlmKs4PlIiqY2+IQuGaY9+ptTe2ih3I9pw1svjSixN0ghpTHi48X0FzI6Dh1zJotKdGlSEN3fcSoHIVMuyyULYd6XN4uT31ytConxLALvYa3fCYUx5kk2xLSbvmKfJOI7x39VOucJDV1iXZ4dL+7ghu//lSvxffiWsSxzFlHoDZJn93Ku3sQzRLc8NKHReF4/kq52TaAyQTT6uZcLE0om6XVNoItzqMpmpQOs0vOEDb6mELtg6CIbEkk/fWo6/j8bbXhu5+cMZJ7hhvmMqQ0ncy/Hfo3PRQSX2ia/uS80qfv/UrkQLVWiv02la7ZsJPAKcsHoa65BhdZ0ocl6xmhEzeryNsVkWUdIF5YZB6KjZLlN0zALf36F/uznkmgnCtzy/DDJLLhA5HNLnbZkLfmeLZw80pSxxQpzd9B4pJVCqsNLvzpVU7/r9zYCRk5PheuzObhFdVxzJ0RVn+SAqODKqzSrEeE5vgzLOmUeI8VpDH9JuA56P7plH81gEMSfa203ZQMc324BfRnI0CBYXX2mNsBEGEKvhA/TOPwklGCXyRTND6OWPd27TYiTYmiEI3rR4a3gbXH0j3xVsldYXkDAVSRG1/pcZ+FUrECcnTBDNVml2kmWKKsTp5p+Rixrwj8g+5FI/DZ/zxemZv8z99zz+TViFc/+SEyBtnLgDLFdH19gm5dH2x+56t4u0Eokg7eg5g9uORREJlo390MUgo+MsKDncVHMIirHznwJZKOQlvgRci6CzYsSN5328UJf0t2B9SliFbEwjauBLgW0beMAc5tq/OO7z3KP894jk3++uwkhlgiTNFIMDT81Kd56k7eC5OPmljLzv/2J5RZ5zbE8SK49UTLpFtRCVQiWKPYG30Tew3fsIah6w==
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
Archive powered by MHonArc 2.6.18.