babioles de renommages

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

4 files changed, 21 insertions, 9 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 3540e9b2a1..b6eae0a1da 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -197,12 +197,22 @@ let pp_logical_ind r =
 let pp_singleton_ind r = 
   pp_comment (Printer.pr_global r ++ str " : singleton inductive constructor")
 
+let set_globals () = match lang () with 
+  | Ocaml -> 
+      keywords := Ocaml.keywords; 
+      global_ids := Ocaml.keywords
+  | Haskell -> 
+      keywords := Haskell.keywords;
+      global_ids := Haskell.keywords
+  | _ -> ()
+
 (*s Extraction to a file. *)
 
 let extract_to_file f prm decls =
-  let preamble,keyw = match lang () with 
-    | Ocaml -> Ocaml.preamble,Ocaml.keywords
-    | Haskell -> Haskell.preamble,Haskell.keywords
+  set_globals ();
+  let preamble = match lang () with 
+    | Ocaml -> Ocaml.preamble    
+    | Haskell -> Haskell.preamble
     | _ -> assert false 
   in 
   let pp_decl = match lang (),prm.modular with 
@@ -224,8 +234,6 @@ let extract_to_file f prm decls =
   cons_cofix := Refset.empty;
   current_module := prm.mod_name;
   Hashtbl.clear renamings;
-  keywords := keyw;
-  global_ids := keyw; 
   let cout = match f with 
     | None -> stdout
     | Some f -> open_out f in
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 12424612cd..0076b99e05 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -26,6 +26,8 @@ val pp_logical_ind : global_reference -> std_ppcmds
 
 val pp_singleton_ind : global_reference -> std_ppcmds
 
+val set_globals : unit -> unit
+
 val extract_to_file : 
   string option -> extraction_params -> ml_decl list -> unit
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index d02f9fb329..3ff34c8b8c 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -246,6 +246,7 @@ let _ =
     (function 
        | [VARG_CONSTR ast] ->
 	   (fun () -> 
+	      set_globals ();
 	      let c = Astterm.interp_constr Evd.empty (Global.env()) ast in
 	      match kind_of_term c with
 		(* If it is a global reference, then output the declaration *)
@@ -286,7 +287,8 @@ let lang_suffix () = match lang () with
 
 let filename f = 
   let s = lang_suffix () in 
-  if Filename.check_suffix f s then Some f,id_of_string (Filename.chop_suffix f s) 
+  if Filename.check_suffix f s then 
+    Some f,id_of_string (Filename.chop_suffix f s) 
   else Some (f^"."^s),id_of_string f
 
 let lang_error () = 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 1df26acc86..6ec52278a7 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -155,9 +155,9 @@ let rec pp_type par vl t =
 	(match collapse_type_app l with
 	   | [] -> assert false
 	   | [t] -> pp_rec par t
-	   | t::l -> (pp_tuple (pp_rec false) l ++ 
-			sec_space_if (l <>[]) ++ 
-			pp_rec false t))
+	   | [t;u] -> pp_rec true u ++ spc () ++ pp_rec false t 
+	   | t::l -> (pp_tuple (pp_rec false) l ++ spc () ++  
+		      pp_rec false t))
     | Tarr (t1,t2) ->
 	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
 	   pp_rec false t2 ++ close_par par)