From 00a05aea070121103baba2c03485127369f24538 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 23 Nov 2014 11:44:31 +0100
Subject: 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.
---
 kernel/nativevalues.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/nativevalues.ml')

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)
-- 
cgit v1.2.3