From 570668efcd61800a5de13d33ab4f2fefc78cc62c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 16 Jun 2010 13:09:43 +0000
Subject: Extraction: fix the eta reduction function used in code optimisations

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

(limited to 'plugins')

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 034baad955..ed4b17dda1 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -601,7 +601,7 @@ let eta_red e =
 	  if m = n then
 	    [], f, a
 	  else if m < n then
-	    snd (list_chop (n-m) ids), f, a
+	    list_skipn m ids, f, a
 	  else (* m > n *)
 	    let a1,a2 = list_chop (m-n) a in
 	    [], MLapp (f,a1), a2
-- 
cgit v1.2.3