Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] folding under binders

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] folding under binders


Chronological Thread 
  • 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.



Archive powered by MHonArc 2.6.18.

Top of Page