| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-19 | coqchk: fix check for kelim with functors | Gaëtan Gilbert | |
| 2018-12-12 | checker: check inductive types by roundtrip through the kernel. | Gaëtan Gilbert | |
| 2018-11-23 | Fix #8937: inductive conversion in coqchk subtyping | Gaëtan Gilbert | |
| As far as I can tell this is similar to what coqtop does. Delta resolvers are complicated so I may be mistaken. The important part is to avoid losing the modified delta resolver returned by strengthen_and_subst in check_mexpr. | |||
| 2018-11-05 | Merge PR #8874: Fix #8873: coqchk on inductive with letin parameter | Pierre-Marie Pédrot | |
| 2018-11-05 | Merge PR #8882: Fix #8881: validate fails to use inductive equivalence in ↵ | Pierre-Marie Pédrot | |
| case_info | |||
| 2018-10-31 | Fix #8881: validate fails to use inductive equivalence in case_info | Gaëtan Gilbert | |
| See also 55dbe8e2fa7ed2053ecd54140f6bcbdf31981e0b | |||
| 2018-10-31 | Fix #8876: expected number of arguments for cumulative constructors | Gaëtan Gilbert | |
| ee573583701c8e53e8b82978998a9df93170cd79 ported to the checker. | |||
| 2018-10-31 | Fix #8873: coqchk on inductive with letin parameter | Gaëtan Gilbert | |
| 2018-09-26 | [ocaml] Update required OCaml version to 4.05.0 | Emilio Jesus Gallego Arias | |
| Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml version so it makes sense we bump our dependency to 4.05.0 as we can use some newer compiler features. | |||
| 2018-07-24 | Fix #7329: coqchk Include with primitive projections | Gaëtan Gilbert | |
| 2018-06-04 | Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵ | Matthieu Sozeau | |
| coinductive types. | |||
| 2018-05-24 | Fix #7323: coqchk puts polymorphic univs of inductive in global env | Gaëtan Gilbert | |
| 2018-05-18 | Fix #7539: Checker does not properly handle negative coinductive types. | Pierre-Marie Pédrot | |
| The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection. | |||
| 2018-04-23 | Fix #7327: coqchk subtyping of polymorphic constants | Gaëtan Gilbert | |
| 2018-04-20 | Fix #6798: coqchk ignores ugraph when comparing constant instances | Gaëtan Gilbert | |
| 2018-03-09 | Delayed weak constraints for cumulative inductive types. | Gaëtan Gilbert | |
| 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. | |||
| 2018-03-09 | Allow using cumulativity without forcing strict constraints. | Gaëtan Gilbert | |
| 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. | |||
| 2018-01-25 | Add test case for #5747 | Maxime Dénès | |
| 2018-01-20 | Adding a test for coqchk bug #6619. | Pierre-Marie Pédrot | |
| 2017-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin | |
| 2017-07-31 | Change the option for cumulativity | Amin Timany | |
| 2017-06-16 | Clean up universes of constants and inductives | Amin Timany | |
| 2017-06-16 | Move (part of) tests from checker to success | Amin Timany | |
| 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. | |||
| 2017-06-16 | Checker add test for non-trivial constraints | Amin Timany | |
| 2017-06-16 | Change the option to Set Inductive Cumulativity | Amin Timany | |
| This requires to change the status of Inductive (we have also changed CoInductive and Variant) from keyword to identifier. | |||
| 2017-06-16 | Correct coqchk reduction | Amin Timany | |
| 2017-05-30 | Add test-suite checks for coqchk with constraints | Jason Gross | |
| 2015-07-07 | Checker: Fix bug #4282 | Matthieu Sozeau | |
| Adapt to new [projection] abstract type comprising a constant and a boolean. | |||
| 2014-12-26 | new test for coqchk | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |