The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Great, thanks Théo!

On Tue, Nov 6, 2018 at 7:15 AM Théo Zimmermann <theo.zimmi AT gmail.com> wrote:

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