begin a test suite

Test that https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38 doesn't regress, and also add some tests for solve_proper because I remember being annoyed at some point that I had to go all the way to Iris to test even the most basic functionality.

changed the description

LGTM. Thanks a lot for this MR!

It seems the tests are not executed on Coq 8.6 as that does not support the hook I am using. Do we care?

I don't.

I also don't mind dropping support for Coq 8.6.

Well I think we can keep it as long as it keeps working...

mentioned in commit 6be2994e

merged