Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] gprogress tactical?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] gprogress tactical?


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] gprogress tactical?
  • Date: Mon, 26 Jan 2015 14:40:00 -0500

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


Archive powered by MHonArc 2.6.18.

Top of Page