The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Ian Lynagh wrote:
> I'm having trouble with high memory usage. I've attached a
> self-contained cut-down example that cann't be compiled in 900 MB:
>    

The usual easy way to reduce memory usage is with the [abstract] 
tactical.  You could wrap each [destruct something; aTactic] piece like 
[abstract (destruct something; aTactic)].  This is only going to work if 
[aTactic] finishes the proof for each case.