aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coqchk
AgeCommit message (Expand)Author
2018-01-20Adding a test for coqchk bug #6619.Pierre-Marie Pédrot
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-31Change the option for cumulativityAmin Timany
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Move (part of) tests from checker to successAmin Timany
2017-06-16Checker add test for non-trivial constraintsAmin Timany
2017-06-16Change the option to Set Inductive CumulativityAmin Timany
2017-06-16Correct coqchk reductionAmin Timany
2017-05-30Add test-suite checks for coqchk with constraintsJason Gross
2015-07-07Checker: Fix bug #4282Matthieu Sozeau
2014-12-26new test for coqchkEnrico Tassi