correction du debut d'optimisation du Fix

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2148 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 14 deletions

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 187df32a4..e9dd12833 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -330,25 +330,27 @@ let collect_lambda =
   in 
   collect []
 
-
-
-let test_eta l =
+let test_eta n l =
   let rec test n = function 
     | [] -> true
-    | a :: q -> a = (MLrel n) || (test (succ n) q)
-  in test 1 l 
+    | a :: q -> a = (MLrel n) && (test (succ n) q)
+  in (List.length l = n) && (test 1 l) 
 
 let optimize_fix a = 
-  if not (optim()) then a else
+  if not (optim()) then a 
+  else
     let lams,b = collect_lambda a in 
-    (match a with 
-      | MLfix(_,[|_|],[|c|]) -> a (* TODO *)
-      | MLapp(b,ids) -> 
-	  (match b with 
-	     | MLfix(_,[|_|],[|_|]) when (test_eta ids)-> b
-	     | MLfix(_,[|_|],[|_|]) -> a (* TODO *)
-	     | _ -> a)
-      | _ -> a)
+    let nlams = List.length lams in 
+    if nlams = 0 then a 
+    else  
+      (match b with 
+	 | MLfix(_,[|_|],[|c|]) -> a (* TODO *)
+	 | MLapp(b,ids) -> 
+	     (match b with 
+		| MLfix(_,[|_|],[|_|]) when (test_eta nlams ids)-> b
+		| MLfix(_,[|_|],[|_|]) -> a (* TODO *)
+		| _ -> a)
+	 | _ -> a)
 
 let normalize_decl = function
  | Dglob (id, a) -> Dglob (id, normalize a)