aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coqchk
Commit message (Collapse)AuthorAge
* Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵Gravatar Matthieu Sozeau2018-06-04
|\ | | | | | | coinductive types.
* | 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
| | | | | | | | | | The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection.
* | 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
| | | | | | | When comparing 2 irrelevant universes [u] and [v] we add a "weak constraint" [UWeak(u,v)] to the UState. Then at minimization time a weak constraint between unrelated universes where one is flexible causes them to be unified.
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | | | | | | | | | | | | | | | | | | Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible.
* 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
| | | | | | Due to some unknown problem coqchk fails on some inductive types when it is compiled with ocaml4.02.3+32bit and camlp5-4.16 which is the case for Travis tests.
* Checker add test for non-trivial constraintsGravatar Amin Timany2017-06-16
|
* Change the option to Set Inductive CumulativityGravatar Amin Timany2017-06-16
| | | | | This requires to change the status of Inductive (we have also changed CoInductive and Variant) from keyword to identifier.
* 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
| | | | | Adapt to new [projection] abstract type comprising a constant and a boolean.
* new test for coqchkGravatar Enrico Tassi2014-12-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 05:35:54 +0000