coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Set Proof Using Clear Unused

From: Théo Zimmermann <theo AT irif.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Set Proof Using Clear Unused
Date: Wed, 3 Feb 2021 09:02:44 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo AT irif.fr; spf=Pass smtp.mailfrom=theo AT irif.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
Ironport-phdr: 9a23:4oLNpRTt/Q0SF3EfQhKEJ/pFgdpsv+yvbD5Q0YIujvd0So/mwa6zYBKN2/xhgRfzUJnB7Loc0qyK6vGmBTVLuM7b+DBaKdoQDkBD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrs1xxfTrXZEZutayX50KV6Ngh3w4tu88IN5/ylfpv4s9dRMXbnmc6g9ULdVECkoP2cp6cPxqBLNVxGP5nwSUmUXlhpHHQ3I5wzkU5nyryX3qPNz1DGVMsPqQ780Xy+i77pwRx/zlCgHLT85/3rJhcF2kalWvQiupx17w47TfYGVKP9zdb7TcN8GWWZMWNtaWjdfCY2gcYQAE+sBPf5Zr4bjoVsOsQC+DhSoCO/21zNEmmP60ag83u88Ew/JwRYgEsoBv3Tartr7NKkcX+OowqfW0TrNYOhb2Svk6IXSbhwtve2AULB2fMHMyUcvDQTFjlCIpIL7PzOSzOMNvHCY4OphUOKvjnAoqxt0oje1wMcsjJTCi4UJylDE6yp5x504JdyiSE56b96oCpVQtzuDOoZwX8gtTH1mtjwgxb0apZ60YjIKyJI/yhPQa/KLbZaE7Bz+WOqMPTp0mW5pdbK7ihi88UWuyunxW9Wo3VhEsCZLksXAu20N2hHR98SLVvtz81m81DuO2Q3e7PxPL04zlareMZEhw7gwm4IcsUTCAi/2mFj2g7SMeko4/eio7vzrbanhpp+GMY97lAX+MqA0lsOhHOs4Lw4DVHWY9+SkzLDv4En0TbpQgvEokqTUv4rWKMUGqqKjHgNY3IUu5w6hAzu61NkUh3oKIVJfdB6Zk4TkOEvCLO36APuhhVmnjS1lyOrcPrL7B5XANnjDn6nlfbZ680Ncyw0zzcpY55JQFL4BPuj/WlL3tNzZEB81KhS0zPz9CNV8zYMTW3iDAqGDMK/KsF+I4PwgI/WUaYMIvDvwJOIp6+DugHI2g1MQfLSl0YEKZH22HflqO0CZbmDtgtcFH2cKpA0+TOnyhV2eUT5ceXGyUrk95jEhCYKmA53PRo63gLCZxie0AoVWZnxaClCLCXrna4KEW+4VZC2OJs9hjycLWKO6S44h0BGurBX1x6BmLurS4C0YtIjs2MJ75+3JxlkO8mlfCN3V+GWQRSkglWQRAjQywapXoEpny17F37Iu0NJCEtkG2/PIVTAINJvZwvZ/Atb0ElbdftqOYFe8Q9vgDytnHYF5+MMHf0soQ4bqtRvExSf/RuZNz+XWVqxxybrV2j3KH+g4y3vC0/N93VohWMxLOHPgm6h+6U3LDpTIiBrfmbz4Lf1Njh6Iz3+KyC+1hG8dVQdxVavfWnVONErMrNq/6FmQFubyW4RiCRNIzIu5EoUPcsfg3AdHXvbtftrEMTq8

This flag was removed in 8.10 as part of the following PR that both
documented and removed undocumented flags and options.

Enrico said about this undocumented flag:

>Set Proof Using Clear Unused is not documented because it its effect is
>problematic, see https://github.com/coq/coq/pull/883 and
>https://github.com/coq/coq/issues/6254.
>I'm fine removing this option.

Despite the undocumented nature of the removed options, there should
probably have been a changelog entry about the removals.

I've never used this flag, so I cannot comment on recommending an alternative.

Théo

Le mar. 2 févr. 2021 à 23:42, Abhishek Anand
<abhishek.anand.iitg AT gmail.com> a écrit :
>
> 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