From dfba2039b7352dbcfb3858bad2d201f54d16e3e2 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 23 Apr 2001 14:46:12 +0000
Subject: Gros nain avec de Bruijn...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1668 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/mlutil.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 89dcd07c5a..6b0213c67f 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -181,7 +181,7 @@ let rec betaiota = function
 		| 0 -> betaiota (MLapp (ml_pop t, List.tl a'))
 		| 1 -> betaiota (MLapp (ml_subst (List.hd a') t, List.tl a'))
 		| _ -> betaiota (MLletin (id, List.hd a', 
-					  MLapp (t, List.tl a'))))
+					  MLapp (t, List.map (ml_lift 1) (List.tl a')))))
 	 (* application of a let in: we push arguments inside *)
 	 | MLletin (id,e1,e2) ->
 	     MLletin (id, e1, betaiota (MLapp (e2, List.map (ml_lift 1) a')))
-- 
cgit v1.2.3