amelioration de la generation des unsafeCoerce

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

1 files changed, 7 insertions, 3 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 7507296600..d03cd00fd8 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -352,7 +352,7 @@ let preamble prm = match lang () with
   | Ocaml -> Ocaml.preamble prm   
   | Haskell -> Haskell.preamble prm
   | Scheme -> Scheme.preamble prm
-  | Toplevel -> (fun _ _ -> mt ())
+  | Toplevel -> (fun _ _ _ -> mt ())
 
 let preamble_sig prm = match lang () with 
   | Ocaml -> Ocaml.preamble_sig prm   
@@ -385,9 +385,13 @@ let print_structure_to_file f prm struc =
     else (create_mono_renamings struc; [])
   in 
   let print_dummys =
-    (struct_ast_search MLdummy struc, 
+    (struct_ast_search ((=) MLdummy) struc, 
      struct_type_search Tdummy struc, 
      struct_type_search Tunknown struc)
+  in 
+  let print_magic = 
+    if lang () <> Haskell then false 
+    else struct_ast_search (function MLmagic _ -> true | _ -> false) struc
   in
   (* print the implementation *)
   let cout = option_app (fun (f,_) -> open_out f) f in 
@@ -395,7 +399,7 @@ let print_structure_to_file f prm struc =
     | None -> !Pp_control.std_ft
     | Some cout -> Pp_control.with_output_to cout in 
   begin try 
-    msg_with ft (preamble prm used_modules print_dummys);
+    msg_with ft (preamble prm used_modules print_dummys print_magic);
     msg_with ft (pp_struct struc);
     option_iter close_out cout; 
   with e ->