diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-07-29 19:41:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-07-29 19:41:46 +0200 |
| commit | dabe6d0e1d1782d3e9647e04aa1bf161765ad882 (patch) | |
| tree | e0ac77d200c301b08e2f0532993de6d6e3ab1862 /CHANGES | |
| parent | 81c19bdd631fa72afa0cac5c8b915d836e0646df (diff) | |
| parent | 639eecd27e42c7dd646afdcb67b5a4e51a4541c1 (diff) | |
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 9 |
1 files changed, 9 insertions, 0 deletions
@@ -85,7 +85,16 @@ 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. +- #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 =============================== |