aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coqchk
AgeCommit message (Expand)Author
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2018-12-19coqchk: fix check for kelim with functorsGaëtan Gilbert
2018-12-12checker: check inductive types by roundtrip through the kernel.Gaëtan Gilbert
2018-11-23Fix #8937: inductive conversion in coqchk subtypingGaëtan Gilbert
2018-11-05Merge PR #8874: Fix #8873: coqchk on inductive with letin parameterPierre-Marie Pédrot
2018-11-05Merge PR #8882: Fix #8881: validate fails to use inductive equivalence in cas...Pierre-Marie Pédrot
2018-10-31Fix #8881: validate fails to use inductive equivalence in case_infoGaëtan Gilbert
2018-10-31Fix #8876: expected number of arguments for cumulative constructorsGaëtan Gilbert
2018-10-31Fix #8873: coqchk on inductive with letin parameterGaëtan Gilbert
2018-09-26[ocaml] Update required OCaml version to 4.05.0Emilio Jesus Gallego Arias
2018-07-24Fix #7329: coqchk Include with primitive projectionsGaëtan Gilbert
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-01-31 08:07:45 +0000