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 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




Archive powered by MHonArc 2.6.18.

Top of Page