aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coqchk
AgeCommit message (Expand)Author
2018-06-04Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...Matthieu Sozeau
2018-05-24Fix #7323: coqchk puts polymorphic univs of inductive in global envGaëtan Gilbert
2018-05-18Fix #7539: Checker does not properly handle negative coinductive types.Pierre-Marie Pédrot
2018-04-23Fix #7327: coqchk subtyping of polymorphic constantsGaëtan Gilbert
2018-04-20Fix #6798: coqchk ignores ugraph when comparing constant instancesGaëtan Gilbert
2018-03-09Delayed weak constraints for cumulative inductive types.Gaëtan Gilbert
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-01-25Add test case for #5747Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-02 19:47:44 +0000