diff options
| author | Maxime Dénès | 2014-11-23 11:44:31 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2014-11-23 11:44:31 +0100 |
| commit | 00a05aea070121103baba2c03485127369f24538 (patch) | |
| tree | 3511347375414d3a2bc15c4ccc9a532f6c375a86 /dev/db | |
| parent | c3bb115fa765278bc3bcb3beb8c74b0fb8b35d98 (diff) | |
Fix #3824. de Bruijn error in normalization of fixpoints.
This bug was affecting the VM and the native compiler, but only in the pretyper
(not the kernel). Types of arguments of fixpoints were incorrectly normalized
due to a missing lift.
Diffstat (limited to 'dev/db')
0 files changed, 0 insertions, 0 deletions