The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi,

Lately I am reading Adam Chlipala's Coq book and experimenting with the 
crush tactic, which seems very useful.

I do have one question: could the crush tactic be extended to call 
constructor? In several proofs I've ended up with situations like this:

crush ; constructor.

And I thought that constructor was a relatively "safe" tactic that crush 
could probably try just to see if it works. Is this not the case?

Best regards,

Michael

--
Print XML with Prince!
http://www.princexml.com