coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.9+beta1 is out!

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr, Théo Zimmermann <theo.zimmi AT gmail.com>
Subject: Re: [Coq-Club] Coq 8.9+beta1 is out!
Date: Fri, 16 Nov 2018 15:59:51 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT juno.mpi-klsb.mpg.de
Ironport-phdr: 9a23:zqB2eh/TqsR3dP9uRHKM819IXTAuvvDOBiVQ1KB40ewcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgL2hicJNzA382/ZhcJ/g61ZvB2vqAdyw5LWbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoUTFeUBOehYpJT5qVsTqxu+ChSnCeTtyj9VgH/20rY30+E5EQHHxQAgBNwPsG/OoNXyLqcSXvm4wa/VxjvAd/NbwSrx5YbMfxw7vP2BWah8fMnQxEU1GA7Jkk2cpZHrMj6RzOgBrmyW4/B9We+uiGMrsQN8rzupy8wxkIfGnJgVxUrB9ShhwIY6O9m4SEljbN6mDZtQsSaaO5FzQsM6QmFkoSU6yrkduZGgZiQKzYwnxxHFZ/OabYeE+hPjVOCPLjdknH9pZbyyihKo/US9zuDwTMq53VdQoidKjtXArnUN2AbS6siDRPt95ECh2TOX2gDR9+FEJ080mLHeK545w748j4ETsErYHiPsn0X2lqCWel0++ue08+TnfqnmppiEOoBojQH+K70ildC7AeQlKQcDRHOb+OS51L3750L1WrRKjvsskqnYqp/WP8obprTqSzNSh40k8lO0Cyqs+NUeh3gOalxfPFq7jwnuDGPPJfX1F/K2hVLkxCtryveALLzkB5TlIX3KkbOndrF4vR1y0g02mOpW45wcKKwHL7qnWFL3u/TdFh58KBOvheH9B4MuhcslRWuTD/rBY+vpuliS67d3erjeVMouoD/4bsMdybvrhH49l0UaePDyj54PaTWjAe8gJF+WMyO13oUxVFwStw97d9TEzUWYWGcINXOqXucn+Sp9D5ipX9+aG9KdxYeZ1SL+JaV4I2BLDlfWSyXqaoODHfIUaWeRJtRr1DkcWv6tRt152A==

Hi,

>> What is |#[local]|? Why is there now support for a deprecated thing?
>
> Guillaume, could you upload the manual so that we can point people to it?
> Essentially #[local] is the same as Local and we advise not to rely on
> it as the feature is completely experimental and the syntax may change.
> Support for the deprecated attribute means that a deprecated attribute
> may be attached to tactics defined with Ltac or Tactic Notation to mark
> them as deprecated. Again, this is documented in the manual (but it is
> not online yet).

Do you mean a #[deprecated] attribute? What you wrote ("a deprecated
attribute") makes it look like deprecated here is an adjective referring to
attribute... Hence me and I guess Beta as well were confused by that changelog
statement.

Kind regards,
Ralf

[Coq-Club] Coq 8.9+beta1 is out!, Guillaume Melquiond, 11/06/2018
- Re: [Coq-Club] Coq 8.9+beta1 is out!, Beta Ziliani, 11/06/2018
  - Re: [Coq-Club] Coq 8.9+beta1 is out!, Théo Zimmermann, 11/06/2018
    - Re: [Coq-Club] Coq 8.9+beta1 is out!, Beta Ziliani, 11/06/2018
    - Re: [Coq-Club] Coq 8.9+beta1 is out!, Clément Pit-Claudel, 11/06/2018
    - Re: [Coq-Club] Coq 8.9+beta1 is out!, Ralf Jung, 11/16/2018
      - Re: [Coq-Club] Coq 8.9+beta1 is out!, Théo Zimmermann, 11/16/2018
- Re: [Coq-Club] Coq 8.9+beta1 is out!, Théo Zimmermann, 11/08/2018