coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Coq 8.6 change poll, Pierre-Marie Pédrot, 05/31/2016
- Re: [Coq-Club] Coq 8.6 change poll, Jonathan Leivent, 05/31/2016
- Re: [Coq-Club] Coq 8.6 change poll, Pierre-Marie Pédrot, 05/31/2016
- Re: [Coq-Club] Coq 8.6 change poll, Jonathan Leivent, 05/31/2016
- Re: [Coq-Club] Coq 8.6 change poll, Pierre-Marie Pédrot, 05/31/2016
- Re: [Coq-Club] Coq 8.6 change poll, Jason Gross, 05/31/2016
- Re: [Coq-Club] Coq 8.6 change poll, Jonathan Leivent, 05/31/2016
Archive powered by MHonArc 2.6.18.