aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coqchk
Commit message (Expand)AuthorAge
* Delayed weak constraints for cumulative inductive types.Gravatar Gaëtan Gilbert2018-03-09
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* Add test case for #5747Gravatar Maxime Dénès2018-01-25
* Adding a test for coqchk bug #6619.Gravatar Pierre-Marie Pédrot2018-01-20
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
* Change the option for cumulativityGravatar Amin Timany2017-07-31
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Move (part of) tests from checker to successGravatar Amin Timany2017-06-16
* Checker add test for non-trivial constraintsGravatar Amin Timany2017-06-16
* Change the option to Set Inductive CumulativityGravatar Amin Timany2017-06-16
* Correct coqchk reductionGravatar Amin Timany2017-06-16
* Add test-suite checks for coqchk with constraintsGravatar Jason Gross2017-05-30
* Checker: Fix bug #4282Gravatar Matthieu Sozeau2015-07-07
* new test for coqchkGravatar Enrico Tassi2014-12-26