The Coq mailing list

[Jasper Stein <jasper AT codeyard.net>]

Op zondag 29 januari 2006 17:14, schreef mulhern:

> But, it takes an unnecessarily long time. My proofs of the subgoals
> already exist in the exact form left after the induction step. Thus,
> "exact <proof1>" will always work when applied to subgoal1 and so
> forth.

There is also the tactic "assumption" which will look in your local context. 
So instead of "auto" you might want to do "assumption; auto" to check for 
hypotheses first, and then applying auto in case it doesn't solve it 
immediately.


Jasper Stein (Team CodeYard)
-- 
(Vragen? Kijk op de website, of anders 
info AT codeyard.net)