correction d'un bug faisant inliner minus, mult, ...

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

2 files changed, 7 insertions, 5 deletions

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index e60765b7e1..b3510e7c17 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -1066,7 +1066,7 @@ let is_not_strict t =
    Futhermore we don't expand fixpoints. *)
 
 let inline_test t = 
-  not (is_fix t) && (ml_size t < 12 && is_not_strict t)
+  not (is_fix (eta_red t)) && (ml_size t < 12 && is_not_strict t)
 
 let manual_inline_list = 
   let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in 
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index cd3134a7e1..0726cd2507 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 i = 
+let dfix_to_mlfix rv av = 
   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,7 +343,8 @@ let dfix_to_mlfix rv av i =
   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 MLfix(i, ids, c)
+  in 
+  fun i -> MLfix(i, ids, c)
 
 let rec optim prm s = function
   | [] -> []
@@ -381,9 +382,10 @@ 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 
       for i = 0 to Array.length rv - 1 do 
-	if inline rv.(i) av.(i)
-	then s := KNmap.add (kn_of_r rv.(i)) (dfix_to_mlfix rv av i) !s
+	if inline rv.(i) (mlfix i)
+	then s := KNmap.add (kn_of_r rv.(i)) (mlfix i) !s
 	else all := false
       done; 
       if !all && top && not prm.modular