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 /kernel/nativevalues.ml | |
| 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 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 51bf4c2738..56dac4ecdf 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -54,7 +54,8 @@ type atom = | Asort of sorts | Avar of identifier | Acase of annot_sw * accumulator * t * (t -> t) - | Afix of t array * t array * rec_pos * int + | Afix of t array * t array * rec_pos * int + (* types, bodies, rec_pos, pos *) | Acofix of t array * t array * int * t | Acofixe of t array * t array * int * t | Aprod of name * t * (t -> t) |