coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] gprogress tactical?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] gprogress tactical?
Date: Mon, 26 Jan 2015 12:02:14 -0800

Is [guard] a new built-in tactical (is it documented?)?

-Jason

On Jan 26, 2015 11:40 AM, "Jonathan Leivent" <jonikelee AT gmail.com> wrote:

On 01/26/2015 02:36 PM, Jonathan Leivent wrote:

That way, [any tac] is [let n:=numsuc tac in guard n=1],

Oops - that should of course be [let n:=numsuc tac in guard n>0].

-- Jonathan

Re: [Coq-Club] gprogress tactical?, (continued)