ml_pop au lieu de ml_lift dans betared_ast

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

3 files changed, 10 insertions, 13 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 8cf08afb18..45f76a3118 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -102,7 +102,8 @@ let globals_of_decl = function
 
 let add_dependency r r' g = 
   let normalize = function
-    | ConstructRef (ip,_) -> IndRef ip
+    | ConstructRef ((sp,_),_) -> IndRef (sp,0)
+    | IndRef (sp,i) as r -> if i = 0 then r else IndRef (sp,0)
     | r -> r
   in
   add_arc (normalize r') (normalize r) g
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 06625a302a..f1876bdc38 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -58,7 +58,7 @@ let ml_liftn k n c =
 
 let ml_lift k c = ml_liftn k 1 c
 
-let pop c = ml_lift (-1) c
+let ml_pop c = ml_lift (-1) c
 
 (*s substitution *)
 
@@ -119,12 +119,14 @@ let rec betared_ast = function
       (match f' with
 	 | MLlam (id,t) -> 
 	     (match nb_occur t with
-		| 0 -> betared_ast (MLapp (ml_lift 1 t, List.tl a'))
+		| 0 -> betared_ast (MLapp (ml_pop t, List.tl a'))
 		| 1 -> betared_ast (MLapp (ml_subst (List.hd a') t,List.tl a'))
-		| _ -> MLapp (f',a'))
+		| _ -> MLletin (id, List.hd a', 
+				betared_ast (MLapp (t, List.tl a'))))
 	 | _ ->
 	     MLapp (f',a'))
-  | a -> ast_map betared_ast a
+  | a -> 
+      ast_map betared_ast a
     
 let betared_decl = function
  | Dglob (id, a) -> Dglob (id, betared_ast a)
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index f788d4809e..cdbf108500 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -196,8 +196,8 @@ let rec pp_expr par env args =
 		    'fNL; 'sTR "  "; pp_pat env pv >];
 	     if args <> [] then [< 'sTR ")" >] else close_par par >]
     | MLfix (i,ids,defs) ->
-	let ids',env' = push_vars ids env in
-      	pp_fix par env' (Some i) (ids',defs) args
+	let ids',env' = push_vars (List.rev ids) env in
+      	pp_fix par env' (Some i) (List.rev ids',defs) args
     | MLexn id -> 
 	[< open_par par; 'sTR "failwith"; 'sPC; 
 	   'qS (string_of_id id); close_par par >]
@@ -319,12 +319,6 @@ let pp_decl = function
       let id = P.rename_global r in
       let env' = ([id], !current_ids) in
       [<  hOV 2 (pp_fix false env' None ([id],[def]) []) >]
-  | Dglob (r, MLfix (n,ids,defs)) ->
-      let ids',env' = push_vars ids (empty_env ()) in
-      [< 'sTR "let "; P.pp_global r; 'sTR " ="; 'fNL;
-	 v 0 [< 'sTR "  "; 
-		hOV 2 (pp_fix false env' (Some n) (ids',defs) []); 
-		'fNL >] >]
   | Dglob (r, a) ->
       hOV 0 [< 'sTR "let "; 
 	       pp_function (empty_env ()) (P.pp_global r) a; 'fNL >]