coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq 8.9+beta1 is out!
Date: Tue, 6 Nov 2018 11:14:44 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f45.google.com
Autocrypt: addr=theo.zimmi AT gmail.com; prefer-encrypt=mutual; keydata= xsFNBFP+V00BEADi9eGxuXfvs0HxaYDxrOBpCJWakA4+lCi3KUGqNS5Xq0V7q+BWZZmF/pOO x4EemIickFV+DA/Yp9542XWw1vMK3uGAUpnB4sUvD+qPDnRFHDZH60p1b8rRzukHRdukW33g QsEjDdNp9iVebuBMe+IU2gdpdZxjgxzxShQMIHOX1Az65oC81eEV37XJ7b89WjArEEe0Hxcg 9+jFH3P3pNdlVaxMgEaYxeepTEfBIhWJjobr299gkgUm2a79vYnci0VONNk3crZqpNvrDK9h bqBgsEUv7t8JnIDQOJTncuoeZA+YFkceYKysO4tyDgNPgXSuI8tUfo7eU1uacNvX7LoKH1nT d4Gr26nPUyj8ntnvnT88LK+CxrrfYkUxtK5pYIQLzJSnCaCuoxOu4WJn+6PPtMhUNWC50fmA +HBt3v8YhheNEEbBZPqEGE9O1A0xB5oJJ3UCsf2VpxiEc3qCTzZHPbw5hYsS96MRysJ3gl9Z OG/u8M5r/JlyiDbVOj6WEcjgMYhuowbEX45UCCufgMWlVFDqKj685zCwhPxYSKvW2+Pkvw1K YmM4tQuF3bH2oQXe8W791N39JXQU/LHD7EHnmoJW/6ySc7Mv2f9cId/HY/DeM1U1TTTEEr1Q j6o/6PdRHGWT5PZpbNDy9+sdBieF1JWuXx24KHbhbN/OCebiewARAQABzSdUaMOpbyBaaW1t ZXJtYW5uIDx0aGVvLnppbW1pQGdtYWlsLmNvbT7CwX0EEwEIACcFAli5dBUCGyMFCQlmAYAF CwkIBwIGFQgJCgsCBBYCAwECHgECF4AACgkQ8XRKCUL1Nsf97A//QpWey31m7X20iHRRO833 BPyziP9QbIQveB8BofZfjWXBJoGExP2EZdb10UMwU0tsnD6NT5E8nKr9rRRTtnwXOcqaQHGd Y4mVLEyJYwZ8g4uZglMyTCHx6k064Ik4c5DysS/15AB72SZm+fJFayIzSY1syvTnTPxTnNx7 l697IbjS3aq3/W+vQ6MwnDgnQqggGMiA0+Tmp5VPCZX9deLmXWC1zeXe/PdCstPzeHTiIHgD wQW+0edCBELbJdhoVBKsQ3OfBK7uMJBXug7zqI3wAoywvd/E12tFzZJhLZiq8arDIimeccf4 bFZUIy17ApiFfAZJU5Rm71H29IFFMTyQxi4QFFiPjWKwtUTDB/Xv6V8nGgdhOHkNgjnRpPn4 jNxSnvr3/f1OW2yGFYyxTUlmYg72eTkSNlPAwd+WA5K3aQQtwUERzhPsK2l4Smjqr7NcI+5X 0aHBVRyRGrTmtTRz/hdyoGoxx4ts1TacquKHx88YH9GZhEng9h+Ak70oQYD9u+atp93wTyTo tghwB5Ewm3O9oruIdQtWx2H4PtP4Y3V1O/DjK42D3wKwikiHisCTKtbuIsgLTnxebWC7wN0q X9nln3KJkEnxZ/6pjLQ3XZB5YeUq58bBnr06VTZYjjYM5aZ6cQrOrnWXvrsrTh367cPKesk5 G5h/itHB0UQc+eXOwU0EU/5XTQEQAL7skL+t5KvE/j2zAzuUFtwjIA+GPBcwOJnITdT3fddN S18gCBx+EH/YPbCphKXOxRFeaD+EDuC1Ls5XK+lYu9hR7rurW7RQI+1XKO7KHQvp4i2I8J4C C+kmMw9K7fysHFG9ckiw1G5WrwiiPZHLadRIAfXwMLoDfRRNu/W8ogjm1m+UWm88DISrkIbE BYEw/fWX8QGGcFvExrFAgXyXXn4vVG90XNre+wJwIADcCqQJXCfzNF/tyetcGEwc3BZiUe/Q Ha/3xLDSm19rDkVWSpWGUr0uSziPSR9kYw6q4F1gKdvex6hnduRMEJLwFRfiHKnHZO2uN8Zj MsB1EklGvkockjkThQfFjeU3zysxfsl4tQRROpglgs1MhiMZpvCdnNTn+Gr+YHQ0sueBxpk0 6GHMmE4C4jcrLFXwfEWOnk6ISHluZS1f9qRnNZzj9ICJItT7cn1KE54jZjmVudi4kOSbihaZ 70PrXMhwphz4nVxSRMIsXdNwSkpCrcOatDS4E7EjRgHW5+CP5WON2aJPD8htAtKNej5nPbTD NFJKz6nG4jdDpxtY0PEkMHarrBpWaIdPEPgdCew5Ns5cAZC0vMkJU8uuSoEumGqzUwdVIWaV p0iZ7MTaWSZeifx7Y6x5YkYR5dMGGzKW5GeLQ7emG0I1BTcFeP+VAGewLA5xWjnhABEBAAHC wWUEGAECAA8FAlP+V00CGwwFCQlmAYAACgkQ8XRKCUL1NscXDRAAx5Y5fyDX/HvFD2Sp4E1h HbtNsPfDQ076U3qvg31e7d5560fW5hwSgZ3++3kGRO7QFTq3edo3oEEWiHuHBJxT7eXSPhXY vsM/atDyQ7Zy6fEUVuv77b3TEDHuWvn4A2kBI+ApCzXohscTuCc/PvVCoDrRQ++be2hIlxsq M7DnRr3/6FI8chCUHj3bXeXtPp8M74/3RGCiwvPZ7825NU0JP6jj1yeEuy6ts/GaZFsDj3sz TxCeZxbdARFxqmT0lf3yF2uQWj35jwqBUC/S+07fZfRRRFXwHTSSzsTTg4JKvsEpq6v0/ryc ETXqwstze+nvPvZ/bLlkiFulLFajYdIky+t5JmjmMEW0/NpK4nRo/QNuTyF1vG1/tjg/q5CZ gW++ZBoYuOR/+roFRPEKIu6Aa843e+QXvpHv4WHN1viH7ufY3D389hKkkhtnEvUu1Mv7ITDD ryw3ok6KFBrjvMQVOp0L7yZc9RYtJ0mXH9n1wWJL94q4hbUJ7fqz2rv8RbTGQoqKfDQVuVuo gH36yLP9s+RKxePuqaTn6DOOHF0/hhMCwes9pWs6ObrEPUVG1YtM6TwopIUJtuLZFWWb3X1Q 4W8EyZElzlCZhLTVhJT7p2k8xBEjpdMpsHhBMjOMljCUeRdJX55g2DVAwx3fvhdOJkuXY5Tl nCgw1L3/lCt46SU=
Ironport-phdr: 9a23:nbiHmBL1aN+KNhwshNmcpTZWNBhigK39O0sv0rFitYgRIvTxwZ3uMQTl6Ol3ixeRBMOHs60C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwdFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhjoZOT438G/ZicJ+g6xUrx2juxNy2IHUbJ2POfR5Yq/Qc9EXSGxcVchRTSxBBYa8YpMRAeoBJ+FYqJHyqFgPrRu7AAmjGvnvyjpSiX/w260xzuMsER3G3AM+GNICqnXVrNTwNKcXUOC416bIzTDZYPNX3Tfx8pTHchckofyVW797bMTfyU4qFwzfj1WQr5ToPzKT1uQXsmiU9fBsVey1i2I/pAFxoySvxscxiobSnI4a1lfE9SB/zY0oJtO4UFZ2bcC4HJZUrS2XNIt7Ttk/T212uys20LILtJ6jcCUJzJkr3QPTZvyGfoSS/B7uVOacLS13iX9qfr+0mgy8/lK6yuLmU8m5yFZKoTRBktnLrn0N0gbc6smDSvdk8Eah3CuD2xnd6uxLIU04j6XbK5kmwr4/kpocr17PETPxmEXzlKOWd0Mk9fa06+n/fLnqupuRO5V3hwz+KKgih9KzDOciPgUBX2WX4eG826fi/U39TrVKlPo2kqzBvZDGJcQUuKm5DxVU04Yi7ha/Cjam3c8XnXkCNl1FeRaHg5L1NFHJJfD0Fe2/jEi0kDd32/DGOaXsDYnKLnjaibvuYbJ961NHxwco1tBe55dUCqkbL/7pW0/xssbYDh4jPACuzebnEoY16oRLUmWWR6SdLan6sFmS5+tpLfPfSpUSvWPBK3ki0MzviHo0g1oUe6/hiYcXZXf+DPVjJkSxbn/lg9NHGmAP6FltBNf2gUGPBGYAL025WLgxs2liWdCWSLzbT4Xou4SvmSKyH5lYfGdDUwneHnLhdoHCUPAJOnvLfp1R1wccXL3kcLcPkAm0vVajmbViJ+vQvCYfsMC7jYUn16jojRg3sAdMIYGd3mWKFTwmm2oJQ3op2fk6rxAgjFiE1qd8jrpTEtkBv/4=
Openpgp: preference=signencrypt

Hi,

On 06/11/2018 11:03, Beta Ziliani wrote:
> Hi devs, I have little questions regarding the changes:
>
> On Tue, Nov 6, 2018 at 6:46 AM Guillaume Melquiond
> guillaume.melquiond AT inria.fr
> <http://mailto:guillaume.melquiond AT inria.fr>
> wrote:
>
> Dear Coq users,
>
> Tactics: introduction tactics intro/intros on a goal that is an
> existential variable now force a refinement of the goal into a
> dependent
> product rather than failing.
>
> Uh,.. why? Will the following tactic endlessly loop? |repeat (intros ?)|

Why would you use repeat (intros ?) instead of intros * exactly?

Anyways, here is the link to the corresponding PR if you want to comment
or see the context: https://github.com/coq/coq/pull/7304
You may also open an issue if you think this PR is bad and should be
reverted.

>
>
>
> Vernacular:
>
> - Experimental support for attributes on commands as in "#[local] Lemma
> foo : bar." Tactics and tactic notations now support the deprecated
> attribute.
>
> 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).

>
> Many thanks,
> Beta
>

Best,
Théo

Attachment: signature.asc
Description: OpenPGP digital signature

[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