coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "now" tactic

From: Thomas Braibant <thomas.braibant AT gmail.com>
To: Jim Apple <coq-club AT jbapple.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "now" tactic
Date: Fri, 18 Mar 2011 07:18:24 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=MsSOhgqV6TizQMQKUVwk0oeyo3+Jw8py8AQgAl1B6KdDQONHZUOTQmkYgVKOQE621U 8dDXnEsGG+qJhOtnEalV7p6jWzLml1625enojY5FQWkwcoXsaEfN+idHF7hkHWAeSKEQ qR+zuyNOuLLnOsLPlDaJSnoWCF16fTd1ZAaz4=

You can find it in Coq.Init.Tactics, along with several other useful
tactics, like "easy", "exfalso", "clear dependent", which are not all
documented.

thomas

On Fri, Mar 18, 2011 at 4:49 AM, Jim Apple
<coq-club AT jbapple.com>
wrote:
> http://coq.inria.fr/cocorico/HowToContributeToTheStandardLibrary
>
> says:
>
> "In long proofs, use now as much as possible when a tactic closes the
> current goal. This improves the robustness of the script. "
>
> I couldn't find "now" in the index of the reference manual:
>
> http://coq.inria.fr/refman/general-index.html
> http://coq.inria.fr/distrib/current/files/Reference-Manual.pdf
>
> Where can I find out what this tactic does?
>

[Coq-Club] "now" tactic, Jim Apple
- Re: [Coq-Club] "now" tactic, Thomas Braibant