The Coq mailing list

["Harley D. Eades III" <harley.eades AT gmail.com>]

Hi. So use sequencing. 

If all the subgoals are generated from[tactic] then use [tactic;try 
congruence]. That will discharge all subgoals solvable by congruence leaving 
the remaining.

Harley



On Apr 25, 2012, at 12:34 PM, 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.