From 1c71ab379c8f860b405a808249d02441bbc66737 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 23 Apr 2001 15:26:10 +0000
Subject: forme code

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

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 6b0213c67f..792952ac3d 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -180,8 +180,9 @@ let rec betaiota = function
 	     (match nb_occur t with
 		| 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.map (ml_lift 1) (List.tl a')))))
+		| _ -> 
+		    let a'' = List.map (ml_lift 1) (List.tl a') in
+		    betaiota (MLletin (id, List.hd a', MLapp (t, 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