Do more checking

Don't coq when we don't have to
Add some code to remove [Abort.]ed goals.
Update TODO

It now reflects the state of things better