search

math-comp / mczify

Micromega tactics for Mathematical Components
23 stars 8 forks source link

Test suite #16

Open pi8027 opened 3 years ago

pi8027 commented 3 years ago

We need a test suite automatically run by CI, and also extensive test cases to detect regressions. I think it makes sense to include example.v in it.

pi8027 commented 3 years ago

We still need extensive test cases to detect regressions. It would also be nice to have more examples demonstrating the usefulness of mczify. Contributions are welcome.

pi8027 commented 3 years ago

I added some more test cases, but there are still many missing cases: https://github.com/math-comp/mczify/blob/8481446a34ee53cf24639210877ed9f7dd1dcf92/examples/test_ssreflect.v