From d68d100a90556b99d4639b2909d1028cbe8db8e2 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 1 Jun 2006 13:53:45 +0000
Subject: reparation bug #1128

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

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index bfff12ef9b..aa74b6cea4 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -981,7 +981,8 @@ let general_optimize_fix f ids n args m c =
   let v = Array.make n 0 in 
   for i=0 to (n-1) do v.(i)<-i done;
   let aux i = function 
-    | MLrel j when v.(j-1)>=0 -> v.(j-1)<-(-i-1)
+    | MLrel j when v.(j-1)>=0 -> 
+	if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
     | _ -> raise Impossible
   in list_iter_i aux args; 
   let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
@@ -1008,8 +1009,7 @@ let optimize_fix a =
 		 -> a'
 	     | MLfix(_,[|f|],[|c|]) -> 
 		 (try general_optimize_fix f ids n args m c
-		  with Impossible -> 
-		    named_lams ids (MLapp (MLfix (0,[|f|],[|c|]),args))) 
+		  with Impossible -> a)
 	     | _ -> a)
       | _ -> a
 
-- 
cgit v1.2.3