Enable test suite to check printed output
Also move test suite out of theories/
so it does not get installed.
I added Show.
in a few random place in the test suite just to have some things that we check not to regress. I also added it to the invariant open tests, because these validate that the from_option
is gone.
@robbertkrebbers if you still remember some of the issues where proofmode simplified too much or not enough, now we could add proper tests for them. :D
Possible issues with this:
- I didn't bother to wire up coqdep with these test files, so if anything in Iris changes, all tests are re-run. That takes <15sec, though.
- tests cannot import other tests any more. However, we didn't make any use of that anyway.