fixes #121 destruct sigma types

[stchang]

This is a temporary fix but it got me thinking, should we disable type checking completely while running tactics? The final term will be type checked anyways right?

[stchang]

fixes #121

[wilbowma]

I could see an argument for yes. It would increase performance, and we ought to only be constructing well-typed terms. However, it might also be useful for debugging tactics.

[stchang]

True. I do see that several tactics raise their own exceptions when given an ill-typed expression, so it may not be completely straightforward to completely disable type checking.

For now, I'll just do it when appropriate for individual tactics.