coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Set Proof Using Clear Unused

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Set Proof Using Clear Unused
Date: Tue, 2 Feb 2021 14:40:37 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f180.google.com
Ironport-phdr: 9a23:SWE/PRy+BlWniMTXCy+O+j09IxM/srCxBDY+r6Qd2ukWIJqq85mqBkHD//Il1AaPAdyKra4cwLeJ++C4ACpcuMnH6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjVu8UMjoZuNqk9xxvLr3BVf+ha2X5kKUickhrh5Mq85oJv/zhVt/k868NOTKL2crgiQ7dFFjomKWc15MPqtRnHUwSC42YXX3sVnBRVHQXL9Qn2UZjtvCT0sOp9wzSaMtbtTb8oQzSi7rxkRwHuhSwaKjM26mDXish3jKJGvBKsogF0zoDIbI2JMvd1Y6XQds4YS2VcRMZcTyNODIOyYYUMEuQPI/pXopLnqFcStxazHxWgCP/txzJOm3T43bc60+MkEQzewAEvBNIOsHXPrNX1KqgSUv2+wbXOzTrZafNZxCr25Y/SfR86ofGMXKlwccrPxkksDQ/KlFOQppbjPzyIzOgNsmmb7/ZvVe+0hG4nrht+ojmrxss2lobJgYcVx0nC+C5kz4k7Oce2R1RnYd64DpRQrSeaOpNoT80iXWxlpSk3xLIbtJKlciUG1pcqygLRZvKHbYSF7RbuWeSMLTp6mX9oeLKxihSx/EWi1uHwSNe43VVJoydLlNTHq34D1xvW6sedS/t9+F+s1iqI1wDJ7OFLP0Q0la7BJ5E/37Ewi5weulnAEC/ugEj6krOae0E+9uWr6+nreKjqq56dOoNulw3zMbgil8qiCuoiKAcORXKU+eGk2b3j40L5RLJKg+UzkqbDsZDaId0Xpq+9AwNIy4oj5QuzAjS63NgCknkHK1VFeB2Dj4f3IV3BPPf4DfKnj1Stljdk2ezGM6X/DpnRKnXPirTscLZn50JByQc+zMpT649XB70dOP7zX1X+tN3cDh83KQy0xOPnBc1n2YwFWWKPA7SZMKPMvl+L/O4gOe+Ma5UTuDngMfQl5v/ujWM2mVIGcqmp2IEYaHG8Hvh8P0qZZn/sjs8bEWgWpgo+UPDqiFqaXDFPYHayRrsw6S0/CIK7FojOXZutgbyE3CejBJJafGFGClaWEXfpbYqIQfkMaDjBavNmxzcDTP2qT5IrnUWlsxa/wL56JMLV/DcZvNTtzo4myffUkEQb/zx1FMSQ0CmkSWhykitcTjU23bt/rE87w1GK16Q+gv1EGvRc4vpIVkExMpuKnL8yMMz7Rg+UJoTBc12hWNjzWWhsHOJ0+McHZgNGI/vnjh3H2HD0UboclrjOBZhtt6yFjyC3KMF6xHLLkqImigt+G5odBSidnqd6sjPrKcvMmkSdmbytcP1FjiHI/WaHi2GJuRMBCVIiYeD+RXkaI3Dug5Hh/EqbFu2hDL0mNk1KzsvQcqY=

Was the following option removed recently:

Set Proof Using Clear Unused.

I get the "unknown option" error (Coq 8.13.0).

Is there a workaround?

Currently, I have to manually clear the unused things at the beginning of proofs so that tactics like tauto/lia ... don't use it unnecessarily. This seems unnecessary work and is implied by the "Proof using ...." directive.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] Set Proof Using Clear Unused, Abhishek Anand, 02/02/2021
- Re: [Coq-Club] Set Proof Using Clear Unused, Théo Zimmermann, 02/03/2021