coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Beta Ziliani <beta AT mpi-sws.org>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Coq 8.9+beta1 is out!
Date: Tue, 6 Nov 2018 07:03:14 -0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT juno.mpi-klsb.mpg.de
Ironport-phdr: 9a23:mM81YhH5TskHCiGiAIrTlp1GYnF86YWxBRYc798ds5kLTJ78oMWwAkXT6L1XgUPTWs2DsrQY07WQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDiwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95eWCxPAIyyb4UBAekcM+hGs4bwvEEBoQekCAS2GO/j1j1Fi3nr1qM6yeQhFgTG0RQ9Et0QrHTbtsj+O6QTUeCxzanH1zPDb/JL0jr684fHbAwhruuXULJ1acrRyFAjFxjLj1WLs4DlOCmV1usUvmWd8uFuW+Wvi2s9pAFwpDii3sYsio/ThoIU0F/I7yt5wJwzKNalS0B7ecapHIZeuiyeLYd6X8cvT3trtSs70LELtoK3cDAUxJg7wxPTcf+KfoiS7h7+VeucIC10iG9kdb+7gRu57FKuxffmVsau1VZHtipFncfItnAKzxHT6NWHSv16/ku73DaPzwHT5vhHIUAwjqrUMIQtwrsolpocq0jMAzH5lF33jK+QaEok5vCl5/npb7jivJOQKot5hhv9P6kvgMCyDvg0PhALX2eB+OS80LPj/Vf+QLVPlvA5ibfWsIzAKskAo665Gw5V3p846xexFDeqytMYnWMILF5dYhKIk5DpO03SIPD/Ffqwn1OskC5yy//aOr3hH47CI2PYkLbheLZ981RTxBAyzdBZ/ZJUC6sOLOj9Wk/r55TkCUoSNBX86OL6Ap0p3YQHHGmLH6WxMaXIsFbO6Ph5cMeWY4pAkjvhIrAX5vrvhHk40QsXcLWg9Z4PaTWjAe8gJF+WNym/yuwdGHsH61JtBNfhj0ePBHsKPy7rDvAMowojAYfjNr/tA4WkgbiPxiC+R8YEY3hHT0uTCjHvbYrWAq5QOhLXGddol3k/bZbkU5UojEr8sRf7jqF4NazT4CJK7cu+hugw3PXakFQJzRIxD8mZ1DvXHWNpmGROQic3maN7ukY7z0+Ml6R10aRV

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 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 ?)

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?

Many thanks,
Beta

[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