diff options
| author | Pierre-Marie Pédrot | 2016-08-17 16:17:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-17 16:17:17 +0200 |
| commit | 13fb26d615cdb03a4c4841c20b108deab2de60b3 (patch) | |
| tree | 55f86d47695ee2071d1f886ce70ad7eec6a1e866 /CHANGES | |
| parent | 3fd0b8ad700bd77aabdd3f3f33b13ba5e93d8bc8 (diff) | |
| parent | bc7ffd368789cb82bb8fc8b642b3de870b92c897 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 12 |
1 files changed, 12 insertions, 0 deletions
@@ -85,13 +85,25 @@ Tools Changes from V8.5pl2 to V8.5pl3 =============================== + +Critical bugfix +- #4876: Guard checker incompleteness when using primitive projections + +Other bugfixes + - #4780: Induction with universe polymorphism on was creating ill-typed terms. +- #4673: regression in setoid_rewrite, unfolding let-ins for type unification. +- #4754: Regression in setoid_rewrite, allow postponed unification problems to remain. +- #4769: Anomaly with universe polymorphic schemes defined inside sections. +- #3886: Program: duplicate obligations of mutual fixpoints Changes from V8.5pl1 to V8.5pl2 =============================== Critical bugfix - Checksums of .vo files dependencies were not correctly checked. +- Unicode-to-ASCII translation was not injective, leading in a soundness bug in + the native compiler. Other bugfixes |