aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coqchk
Commit message (Expand)AuthorAge
* Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...Gravatar Matthieu Sozeau2018-06-04
|\
* | Fix #7323: coqchk puts polymorphic univs of inductive in global envGravatar Gaëtan Gilbert2018-05-24
| * Fix #7539: Checker does not properly handle negative coinductive types.Gravatar Pierre-Marie Pédrot2018-05-18
* | Fix #7327: coqchk subtyping of polymorphic constantsGravatar Gaëtan Gilbert2018-04-23
* | Fix #6798: coqchk ignores ugraph when comparing constant instancesGravatar Gaëtan Gilbert2018-04-20
|/
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-01 23:24:08 +0000