coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to Repeatedly Apply of a Tactic

From: Saint Wesonga <saintwesonga AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] How to Repeatedly Apply of a Tactic
Date: Wed, 25 Apr 2012 11:34:08 -0600

Hello All,

I have a proof with 50 subgoals. Most of them can be dispatched with the "congruence" tactic, but I don't want to have 50 separate congruence commands. I have tried using "do" and "repeat" but those only seem to solve 1 goal. Is there a better way to do this?

Saint.

[Coq-Club] How to Repeatedly Apply of a Tactic, Saint Wesonga
- Re: [Coq-Club] How to Repeatedly Apply of a Tactic, Harley D. Eades III
- Message not available
  - Re: [Coq-Club] How to Repeatedly Apply of a Tactic, Saint Wesonga
- [Coq-Club] Re: How to Repeatedly Apply of a Tactic, Saint Wesonga