coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] gprogress tactical?
- Date: Mon, 26 Jan 2015 12:05:02 -0500
On 01/26/2015 11:48 AM, Jason Gross wrote:
A built-in [any] tactical lets you easily build [gprogress] (and many
others) in ltac, while otherwise a dedicated [gprogress]-like tactic
written in ocaml is needed for each tactic you want to have a global
version of.
A case other than for use with [progress] where an [any] tactical would be useful is for solver tactics that fail if they don't solve the goal. Such as: [any omega] - as that would tell you if omega succeeded in any focused goal or failed in all.
-- Jonathan
- Re: [Coq-Club] gprogress tactical?, (continued)
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/24/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/24/2015
- Re: [Coq-Club] gprogress tactical?, Pierre-Marie Pédrot, 01/25/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/25/2015
- Re: [Coq-Club] gprogress tactical?, Jason Gross, 01/25/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/25/2015
- Re: [Coq-Club] gprogress tactical?, Arnaud Spiwack, 01/26/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] gprogress tactical?, Arnaud Spiwack, 01/26/2015
- Re: [Coq-Club] gprogress tactical?, Jason Gross, 01/26/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] gprogress tactical?, Jason Gross, 01/26/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] gprogress tactical?, Arnaud Spiwack, 01/26/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/25/2015
- Re: [Coq-Club] gprogress tactical?, Pierre-Marie Pédrot, 01/25/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/24/2015
- Re: [Coq-Club] gprogress tactical?, Jonathan Leivent, 01/24/2015
Archive powered by MHonArc 2.6.18.