The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

Hi,

On Thursday 06 December 2007 12:57:46 Marko Malikoviæ wrote:
> Dear all,
>
> I need advice from somebody with experience and who have some feeling what
> the best direction in this situation is:
>
> - tfrom proof of one goal I have lot of subgoals
> - some of the subgoal is possible to prove but some of them is not
> - proved subgoals are not interesting for me but in unproved subgoals I
> have some computed hypotheses which are important for me and with this
> hypothesis I have to recursively reasoning in further steps. Furthermore,
> some hypotheses are missing after first step.
...

Do you have a small example that demonstrates the problem? I don't fully 
understand how you determine which subgoals are interesting and what 
information you care about is lost after a proof step.

Regards,

Sean