coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
- To: Clément Pit-Claudel <cpitclaudel AT gmail.com>
- Cc: coq-club AT inria.fr, Istvan K Chung <ikdc AT mit.edu>
- Subject: Re: [Coq-Club] folding under binders
- Date: Tue, 25 Sep 2018 13:48:20 +0200
Hi Clément,
Thanks a lot for noticing the regression. I made a pull request on
github.com/coq/coq (PR #8553) which fixes it.
Best,
Hugo
On Tue, Sep 25, 2018 at 01:12:30AM -0400, Clément Pit-Claudel wrote:
> On 2018-09-24 23:41, Abhishek Anand wrote:
> > Is there a general advanced fold tactic such that `advanced_fold add2`
> > changes "n+2" to "add2 n"?
>
> I usually use [change (?n + 2) with (add2 n)]. It works in Coq 8.4, but
> unfortunately not in 8.8, apparently. I don't know when it stopped working.
>
> Another similar example from a few months ago still works:
>
> Goal (forall n : nat, ((n >= 0) -> False) -> False) -> True.
> intro.
> repeat change (?a -> False) with (not a) in H.
>
> Clément.
- [Coq-Club] folding under binders, Abhishek Anand, 09/25/2018
- Re: [Coq-Club] folding under binders, Clément Pit-Claudel, 09/25/2018
- Re: [Coq-Club] folding under binders, Hugo Herbelin, 09/25/2018
- Re: [Coq-Club] folding under binders, Clément Pit-Claudel, 09/25/2018
Archive powered by MHonArc 2.6.18.