meme correction de bug, en moins bourrin

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

1 files changed, 6 insertions, 6 deletions

diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 0726cd250..dc65e1a5d 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -329,7 +329,7 @@ let rec subst_glob_ast s t = match t with
   | MLglob (ConstRef kn) -> (try KNmap.find kn s with Not_found -> t)
   | _ -> ast_map (subst_glob_ast s) t
 
-let dfix_to_mlfix rv av = 
+let dfix_to_mlfix rv av i = 
   let rec make_subst n s = 
     if n < 0 then s 
     else make_subst (n-1) (KNmap.add (kn_of_r rv.(n)) (n+1) s)
@@ -343,8 +343,7 @@ let dfix_to_mlfix rv av =
   in 
   let ids = Array.map (fun r -> id_of_label (label (kn_of_r r))) rv in 
   let c = Array.map (subst 0) av 
-  in 
-  fun i -> MLfix(i, ids, c)
+  in MLfix(i, ids, c)
 
 let rec optim prm s = function
   | [] -> []
@@ -382,10 +381,11 @@ let rec optim_se top prm s = function
   | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> 
       let av = Array.map (fun a -> normalize (subst_glob_ast !s a)) av in 
       let all = ref true in 
-      let mlfix = dfix_to_mlfix rv av in 
+      (* This fake body ensures that no fixpoint will be auto-inlined. *)
+      let fake_body = MLfix (0,[||],[||]) in 
       for i = 0 to Array.length rv - 1 do 
-	if inline rv.(i) (mlfix i)
-	then s := KNmap.add (kn_of_r rv.(i)) (mlfix i) !s
+	if inline rv.(i) fake_body
+	then s := KNmap.add (kn_of_r rv.(i)) (dfix_to_mlfix rv av i) !s
 	else all := false
       done; 
       if !all && top && not prm.modular