Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq 8.6 change poll

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.6 change poll


Chronological Thread 
  • From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Coq 8.6 change poll
  • Date: Tue, 31 May 2016 17:23:41 +0200

On 31/05/2016 17:20, Jonathan Leivent wrote:
> This looks really good...
>
> Will it be possible to use Ltac to incrementally build up and break down
> things like simple_intropattern and hyp_list? Or will they stay opaque
> as in 8.5?

I don't think I'll have time to code it for 8.6, but this is definitely
going to land at some point aftewards.

> I did some grepping and found I have only one instance of constr:
> lacking parens - and that is:
>
> Ltac last_hyp := lazymatch goal with H : _ |- _ => constr:H end.
>
> In this case, the "constr:" isn't needed in 8.5. Will that change in
> 8.6? In other words, will it be necessary to enclose all constrs in a
> "constr:(...)" wrapper in 8.6, even those not requiring this in 8.5? It
> will be harder to find such occurrences...

No, Ltac is mostly unchanged on surface, even though there have been
important architectural changes going on that will allow a much richer
and more regular behaviour of Ltac.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page