The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

> It seems like something must be wrong here.  Is there something I
> should be using instead of "inversion H; congruence"?  If nothing
> else, is there way to give CoqIDE more memory so it doesn't crash?

From what I've experienced already, congruence is not the culprit but
inversion may well be. You could try cleaning each subgoal from
useless hypotheses before calling inversion, that would shrink the
proof terms considerably.
Also if you have average-sized objects in your proof (say peano
integers of size ~ 1000) it may be a good idea to abstract them, some
tactics (tauto for instance) will duplicate objects many types and
lead to that kind of
memory issues.

S.
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06