The Coq mailing list

[Saint Wesonga <saintwesonga AT gmail.com>]

Just for curiosity's sake. Is there a way of repeatedly applying a tactic that solves all goals without using the semi-colon method like "inversion; congruence." If I just wanted to say apply the congruence tactic repeatedly until it doesn't solve a goal. Is this doable?

On Wed, Apr 25, 2012 at 11:34 AM, Saint Wesonga <saintwesonga AT gmail.com> wrote:

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.