changements de dernieres minutes pour la 8.1 beta:

- qualification correcte des noms en Haskell
- on imprime les types de toutes les fonctions en Haskell
- en Ocaml, les appels recursifs d'une f : 'a truc doivent 
 se faire avec les _meme_ parametres de types 'a. Exemple illegal: 
   let rec f = function [] -> 0 | l -> f [l];;
 On met maintenant des Obj.magic en conséquence. 
 En Haskell (avec typage fourni), ca passe. 



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

1 files changed, 2 insertions, 7 deletions

diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 15d219e49..18629bcec 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -343,13 +343,9 @@ and pp_pat env i pv =
 and pp_function env f t =
   let bl,t' = collect_lams t in
   let bl,env' = push_vars bl env in
-  let is_function pv =
-    let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in
-    not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl)
-  in
   match t' with 
-    | MLcase(i,MLrel 1,pv) when i=Standard ->
-	if is_function pv then
+    | MLcase(i,MLrel 1,pv) when i=Standard -> 
+	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then 
 	  (f ++ pr_binding (List.rev (List.tl bl)) ++
        	     str " = function" ++ fnl () ++
 	     v 0 (str "  | " ++ pp_pat env' i pv))
@@ -358,7 +354,6 @@ and pp_function env f t =
              str " = match " ++
 	     pr_id (List.hd bl) ++ str " with" ++ fnl () ++
 	     v 0 (str "  | " ++ pp_pat env' i pv))
-	  
     | _ -> (f ++ pr_binding (List.rev bl) ++
 	      str " =" ++ fnl () ++ str "  " ++
 	      hov 2 (pp_expr false env' [] t'))