The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Hello Guillaume,

Thanks for the hint. The Strategy thing looks like it can be very useful at times. In my case I found another solution. I was using the simpl tactic to simplify the hypothesis that I was destruct-ing. Now, instead, I explicitly do unfold and only unfold the things I want to unfold. simpl was also unfolding N.pow. Because of this I now do

destruct (Nlt_ge_dec (i + j) (2 ^ 32))

instead of the

destruct (Nlt_ge_dec (i + j) (N.pos (2 ^ 32)))

that I had before. This no longer computationally explodes at Qed time so it is also a solution to my problem.

Many thanks!

Chris