Reorganisation du pretty-print:

- Dfix sans rename_global
- question du renommage
- code cleanup (plein)

Encore a finir: bug modules/qualification et syntax records


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

9 files changed, 234 insertions, 271 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 3dac36f4df..0501f19b4a 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -25,7 +25,7 @@ open Nametab
 
 let current_module = ref (id_of_string "")
 
-let is_construct = function ConstructRef _ -> true | _ -> false 
+let used_modules = ref []
 
 let long_module r = 
   match modpath (kn_of_r r) with 
@@ -94,7 +94,6 @@ let cache r f =
 
 module ToplevelParams = struct
   let globals () = Idset.empty
-  let rename_global r _ = id_of_global None r
   let pp_global r _ _ = Printer.pr_global r
 end
 
@@ -113,9 +112,7 @@ module MonoParams = struct
     cache r
       (fun r -> 
 	 let id = id_of_global None r in
-	 rename_global_id 
-	   (if upper || (is_construct r) 
-	    then uppercase_id id else lowercase_id id))
+	 rename_global_id (if upper then uppercase_id id else lowercase_id id))
       
   let pp_global r upper _ = 
     str (check_ml r (string_of_id (rename_global r upper)))
@@ -146,19 +143,24 @@ module ModularParams = struct
     cache r 
       (fun r -> 
 	 let id = id_of_global None r in 
-	 if upper || (is_construct r) then 
+	 if upper then
 	   rename_global_id r id (uppercase_id id) "Coq_"
 	 else rename_global_id r id (lowercase_id id) "coq_")
 
+  let qualify m id ctx = 
+    if m = !current_module then false
+    else if ctx = None then true 
+    else if Idset.mem id (out_some ctx) then true 
+    else false 
+      
   let pp_global r upper ctx = 
     let id = rename_global r upper in 
     let m = short_module r in
-    let mem id = match ctx with 
-      | None -> true
-      | Some ctx -> Idset.mem id ctx in 
-    let s = if (m <> !current_module) && (mem id) then 
-      (String.capitalize (string_of_id m)) ^ "." ^ (string_of_id id)
-    else (string_of_id id)
+    let s = string_of_id id in 
+    let s = 
+      if qualify m id ctx then 
+	String.capitalize (string_of_id m) ^ "." ^ (string_of_id id)
+      else string_of_id id 
     in str (check_ml r s)
 
 end
@@ -215,22 +217,22 @@ let extract_to_file f prm decls =
     | _ -> assert false 
   in 
   let pp_decl = pp_decl prm.modular in 
-  let used_modules = if prm.modular then 
-    Idset.remove prm.mod_name (decl_get_modules decls)
-  else Idset.empty
-  in 
   let print_dummys = 
     (decl_search MLdummy decls, 
      decl_type_search Tdummy decls, 
      decl_type_search Tunknown decls) in 
   cons_cofix := Refset.empty;
   current_module := prm.mod_name;
+  used_modules := if prm.modular then 
+    let set = (Idset.remove prm.mod_name (decl_get_modules decls))
+    in Idset.fold (fun m l -> m :: l) set [] 
+  else [];
   Hashtbl.clear renamings;
   let cout = match f with 
     | None -> stdout
     | Some f -> open_out f in
   let ft = Pp_control.with_output_to cout in
-  pp_with ft (preamble prm used_modules print_dummys);
+  pp_with ft (preamble prm !used_modules print_dummys);
   if not prm.modular then 
     List.iter (fun r -> pp_with ft (pp_logical_ind r)) 
       (List.filter decl_is_logical_ind prm.to_appear); 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 9b33046026..283309b59e 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -35,7 +35,7 @@ let preamble prm used_modules (mldummy,tdummy,tunknown) =
   let m = String.capitalize (string_of_id prm.mod_name)   in 
   str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ 
   str "import qualified Prelude" ++ fnl() ++
-  Idset.fold 
+  List.fold_right
     (fun m s -> 
        str "import qualified " ++ pr_id (uppercase_id m) ++ fnl() ++ s)
     used_modules (mt ()) ++ fnl()
@@ -51,16 +51,14 @@ let pp_abst = function
              prlist_with_sep (fun () -> (str " ")) pr_id l ++
              str " ->" ++ spc ())
 
+let pr_lower_id id = pr_id (lowercase_id id)
+
 (*s The pretty-printing functor. *)
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_type_global r = P.pp_global r true None
 let pp_global r = P.pp_global r false None
-
-let rename_global r = P.rename_global r false
-
-let pr_lower_id id = pr_id (lowercase_id id)
+let pp_global_up r = P.pp_global r true None
 
 let empty_env () = [], P.globals()
 
@@ -71,13 +69,13 @@ let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ -> assert false 
     | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
-    | Tglob (r,[]) -> pp_type_global r	
+    | Tglob (r,[]) -> pp_global_up r	
     | Tglob (r,l) -> 
-	open_par par ++ pp_type_global r ++ spc () ++
-	prlist_with_sep spc (pp_type true vl) l ++ close_par par
+	pp_par par 
+	  (pp_global_up r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l)
     | Tarr (t1,t2) ->
-	open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
-	pp_rec false t2 ++ close_par par
+	pp_par par 
+	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy -> str "()"
     | Tunknown -> str "()"
  in 
@@ -93,13 +91,10 @@ let expr_needs_par = function
   | MLcase _ -> true
   | _        -> false 
 
-let rec pp_expr par env args = 
-  let apply st = match args with
-    | [] -> st
-    | _  -> hov 2 (open_par par ++ st ++ spc () ++
-                     prlist_with_sep (fun () -> (spc ())) (fun s -> s) args ++
-                     close_par par) 
-  in
+
+let rec pp_expr par env args =
+  let par' = args <> [] || par
+  and apply st = pp_apply st par args in 
   function
     | MLrel n -> 
 	let id = get_db_name n env in apply (pr_id id)
@@ -110,47 +105,40 @@ let rec pp_expr par env args =
       	let fl,a' = collect_lams a in
 	let fl,env' = push_vars fl env in
 	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
-	if args = [] then
-          (open_par par ++ st ++ close_par par)
-        else
-          apply (str "(" ++ st ++ str ")")
+	apply (pp_par par' st)
     | MLletin (id,a1,a2) ->
+	assert (args=[]);
 	let i,env' = push_vars [id] env in
-	let par' = par || args <> [] in
-	let par2 = not par' && expr_needs_par a2 in
-	apply 
+	let pp_id = pr_id (List.hd i)
+	and pp_a1 = pp_expr false env [] a1
+	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
+	hv 0 
 	  (hv 0 
-	     (hv 0 (open_par par' ++
-		    hov 2 (str "let" ++ spc () ++ pr_id (List.hd i) ++ 
-			   str " = " ++ pp_expr false env [] a1) ++ 
-		    spc () ++ str "in") ++
-	      spc () ++ hov 0 (pp_expr par2 env' [] a2) ++ close_par par'))
+	     (pp_par par 
+		(hov 2 (str "let" ++ pp_id ++ str " = " ++ pp_a1) ++ 
+		 spc () ++ str "in") ++
+	      spc () ++ hov 0 pp_a2))
     | MLglob r -> 
 	apply (pp_global r)
     | MLcons (r,[]) ->
-	assert (args=[]); pp_global r
+	assert (args=[]); pp_global_up r
     | MLcons (r,[a]) ->
 	assert (args=[]);
-	(open_par par ++ pp_global r ++ spc () ++
-	   pp_expr true env [] a ++ close_par par)
+	pp_par par (pp_global_up r ++ spc () ++ pp_expr true env [] a)
     | MLcons (r,args') ->
 	assert (args=[]);
-	(open_par par ++ pp_global r ++ spc () ++
-	   prlist_with_sep (fun () -> (spc ())) (pp_expr true env []) args' ++
-	   close_par par)
+	pp_par par (pp_global_up r ++ spc () ++ 
+		    prlist_with_sep spc (pp_expr true env []) args')
     | MLcase (t, pv) ->
-      	apply
-      	  (if args <> [] then (str "(")  else open_par par ++
-      	     v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
-		    fnl () ++ str "  " ++ pp_pat env pv) ++
-	     if args <> [] then (str ")") else close_par par)
+      	apply (pp_par par' 
+		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
+		       fnl () ++ str "  " ++ pp_pat env pv)))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-      	pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args
+      	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
     | MLexn s -> 
 	(* An [MLexn] may be applied, but I don't really care. *)
-	(open_par par ++ str "Prelude.error" ++ spc () ++ 
-	 qs s ++ close_par par)
+	pp_par par (str "Prelude.error" ++ spc () ++ qs s)
     | MLdummy ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLcast (a,t) -> pp_expr par env args a
@@ -160,40 +148,28 @@ and pp_pat env pv =
   let pp_one_pat (name,ids,t) =
     let ids,env' = push_vars (List.rev ids) env in
     let par = expr_needs_par t in
-    hov 2 (pp_global name ++
-	     begin match ids with 
-	       | [] -> (mt ())
-	       | _  -> (str " " ++ 
-			  prlist_with_sep 
-			    (fun () -> (spc ())) pr_id (List.rev ids))
-	     end ++
-	     str " ->" ++ spc () ++ pp_expr par env' [] t)
+    hov 2 (pp_global_up name ++
+	   (match ids with 
+	      | [] -> mt ()
+	      | _  -> (str " " ++ 
+		       prlist_with_sep 
+			 (fun () -> (spc ())) pr_id (List.rev ids))) ++
+	   str " ->" ++ spc () ++ pp_expr par env' [] t)
   in 
   (prvect_with_sep (fun () -> (fnl () ++ str "  ")) pp_one_pat pv)
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)
 
-and pp_fix par env in_p (ids,bl) args =
-  (open_par par ++ 
-   v 0  
-     (v 2 (str "let" ++ fnl () ++
-	   prvect_with_sep fnl 
-	  (fun (fi,ti) -> pp_function env (pr_id fi) ti) 
-	     (array_map2 (fun a b -> a,b) ids bl)) ++ 
-      fnl () ++ 
-      (match in_p with
-	 | Some j -> 
-      	     hov 2 (str "in " ++ pr_id ids.(j) ++
-		    if args <> [] then
-		      (str " " ++ 
-		       prlist_with_sep (fun () -> (str " "))
-		      (fun s -> s) args)
-		    else
-		      (mt ()))
-	 | None -> 
-	     (mt ()))) ++
-   close_par par)
+and pp_fix par env i (ids,bl) args =
+  pp_par par
+    (v 0  
+       (v 2 (str "let" ++ fnl () ++
+	     prvect_with_sep fnl 
+	       (fun (fi,ti) -> pp_function env (pr_id fi) ti) 
+	       (array_map2 (fun a b -> a,b) ids bl)) ++ 
+	fnl () ++ 
+	hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
 
 and pp_function env f t =
   let bl,t' = collect_lams t in
@@ -206,8 +182,8 @@ and pp_function env f t =
 
 let pp_one_inductive (pl,name,cl) =
   let pl = rename_tvars keywords pl in
-  let pp_constructor (id,l) =
-    (pp_global id ++
+  let pp_constructor (r,l) =
+    (pp_global_up r ++
      match l with
        | [] -> (mt ()) 
        | _  -> (str " " ++
@@ -215,7 +191,7 @@ let pp_one_inductive (pl,name,cl) =
 		  (fun () -> (str " ")) (pp_type true (List.rev pl)) l))
   in
   (str (if cl = [] then "type " else "data ") ++ 
-   pp_type_global name ++ str " " ++
+   pp_global_up name ++ str " " ++
    prlist_with_sep (fun () -> (str " ")) pr_lower_id pl ++
    (if pl = [] then (mt ()) else (str " ")) ++
    if cl = [] then str "= () -- empty inductive"
@@ -236,22 +212,21 @@ let pp_decl = function
   | Dtype (r, l, t) ->
       let l = rename_tvars keywords l in
       let l' = List.rev l in 
-      hov 0 (str "type " ++ pp_type_global r ++ spc () ++ 
+      hov 0 (str "type " ++ pp_global_up r ++ spc () ++ 
 	       prlist_with_sep (fun () -> (str " ")) pr_id l ++
 	       (if l <> [] then (str " ") else (mt ())) ++ str "=" ++ spc () ++
 	       pp_type false l' t ++ fnl ())
   | Dfix (rv, defs,_) ->
-      let ids = List.map rename_global (Array.to_list rv) in 
-      let env = List.rev ids, P.globals() in
+      let ppv = Array.map pp_global rv in 
       (prlist_with_sep (fun () -> fnl () ++ fnl ()) 
-	   (fun (fi,ti) -> pp_function env (pr_id fi) ti)
-	   (List.combine ids (Array.to_list defs)) ++ fnl ())
+	   (fun (pi,ti) -> pp_function (empty_env ()) pi ti)
+	   (List.combine (Array.to_list ppv) (Array.to_list defs)) ++ fnl ())
   | Dterm (r, a, _) ->
       hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl ())
   | DcustomTerm (r,s) -> 
       hov 0  (pp_global r ++ str " =" ++ spc () ++ str s ++ fnl ())
   | DcustomType (r,s) -> 
-      hov 0  (str "type " ++ pp_type_global r ++ str " = " ++ str s ++ fnl ())
+      hov 0  (str "type " ++ pp_global_up r ++ str " = " ++ str s ++ fnl ())
 
 end
 
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 8a0deeca6c..00f09cb145 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -15,6 +15,7 @@ open Miniml
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
+val preamble : 
+  extraction_params -> identifier list -> bool * bool * bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 3945e941ba..62960af7cc 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -78,7 +78,7 @@ type extraction_params =
 module type Mlpp_param = sig
   val globals : unit -> Idset.t
       (* the bool arg is: should we rename in uppercase or not ? *)
-  val rename_global : global_reference -> bool -> identifier
+      (* the identifier set correspond to local bindings to avoid. *)
   val pp_global : global_reference -> bool -> Idset.t option -> std_ppcmds
 end
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 460e661e0f..ac463391b2 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -487,18 +487,17 @@ let ast_subst e =
   in subst 0
 
 (*s Generalized substitution. 
-   [gen_subst v m d t] applies to [t] the substitution coded in the 
-   [v] array: [(Rel i)] becomes [(Rel v.(i))]. [d] is the correction applies 
-   to [Rel] greater than [m]. *)
+   [gen_subst v d t] applies to [t] the substitution coded in the 
+   [v] array: [(Rel i)] becomes [v.(i-1)]. [d] is the correction applies 
+   to [Rel] greater than [Array.length v]. *)
 
 let gen_subst v d t = 
   let rec subst n = function
     | MLrel i as a -> 
 	let i'= i-n in 
 	if i' < 1 then a 
-	else if i' < Array.length v then 
-	  if v.(i') = 0 then MLdummy
-	  else MLrel (v.(i')+n) 
+	else if i' <= Array.length v then 
+	  ast_lift n v.(i') 
 	else MLrel (i+d) 
     | a -> ast_map_lift subst n a
   in subst 0 t
@@ -798,14 +797,13 @@ let kill_some_lams bl (ids,c) =
   let n' = List.fold_left (fun n b -> if b then (n+1) else n) 0 bl in 
   if n = n' then ids,c
   else if n' = 0 then [],ast_lift (-n) c 
-  else begin 
-    let v = Array.make (n+1) 0 in 
+  else begin
+    let v = Array.make n MLdummy in 
     let rec parse_ids i j = function 
       | [] -> ()
-      | true :: q -> 
-	  v.(i) <- j; parse_ids (i+1) (j+1) q
-      | false :: q -> parse_ids (i+1) j q
-    in parse_ids 1 1 bl ; 
+      | true :: l -> v.(i) <- MLrel j; parse_ids (i+1) (j+1) l
+      | false :: l -> parse_ids (i+1) j l
+    in parse_ids 0 1 bl ; 
     select_via_bl bl ids, gen_subst v (n'-n) c
   end
 
@@ -1180,8 +1178,11 @@ let rec optimize prm = function
 and optimize_Dfix prm (r,t,typ) b l = 
   match t with 
     | MLfix (_, f, c) -> 
-	if Array.length f = 1 then 
-	  if b then Dfix ([|r|], c,[|typ|]) :: (optimize prm l)
+	let len = Array.length f in 
+	if len = 1 then 
+	  if b then 
+	    let c = [|ast_subst (MLglob r) c.(0)|] in 
+	    Dfix ([|r|], c, [|typ|]) :: (optimize prm l)
 	  else optimize prm l
 	else 
 	  let v = try 
@@ -1197,6 +1198,9 @@ and optimize_Dfix prm (r,t,typ) b l =
 		(fun r -> try Refmap.find r map
 		 with Not_found -> Tunknown) v 
 	    in 
+	    let c = 
+	      let gv = Array.map (fun r -> MLglob r) v in 
+	      Array.map (gen_subst gv (-len)) c in 
 	    Dfix (v, c, typs) :: (optimize prm l)
 	  else optimize prm l 
     | _ -> raise Impossible
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 72a34a65d7..e62e2e2820 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -28,11 +28,7 @@ let cons_cofix = ref Refset.empty
 
 (*s Some utility functions. *)
 
-let open_par = function true -> str "(" | false -> (mt ())
-
-let close_par = function true -> str ")" | false -> (mt ())
-
-let pp_par par st = function true -> str "(" ++ st ++ str ")" | false -> mt ()
+let pp_par par st = if par then str "(" ++ st ++ str ")" else st
 
 let pp_tvar id = 
   let s = string_of_id id in 
@@ -41,39 +37,39 @@ let pp_tvar id =
   else str ("' "^s)
 
 let pp_tuple_light f = function
-  | [] -> (mt ())
+  | [] -> mt ()
   | [x] -> f true x
-  | l -> (str "(" ++
-      	    prlist_with_sep (fun () -> (str "," ++ spc ())) (f false) l ++
-	    str ")")
+  | l -> 
+      pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l)
+
 
 let pp_tuple f = function
-  | [] -> (mt ())
+  | [] -> mt ()
   | [x] -> f x
-  | l -> (str "(" ++
-      	    prlist_with_sep (fun () -> (str "," ++ spc ())) f l ++
-	    str ")")
+  | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l)
 
 let pp_boxed_tuple f = function
-  | [] -> (mt ())
+  | [] -> mt ()
   | [x] -> f x
-  | l -> (str "(" ++
-      	    hov 0 (prlist_with_sep (fun () -> (str "," ++ spc ())) f l ++
-		     str ")"))
+  | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
 
 let pp_abst = function
-  | [] -> (mt ())
-  | l  -> (str "fun " ++
-             prlist_with_sep (fun () -> (str " ")) pr_id l ++
-             str " ->" ++ spc ())
+  | [] -> mt ()
+  | l  -> 
+      str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++ 
+      str " ->" ++ spc ()
+
+let pp_apply st par args = match args with
+  | [] -> st
+  | _  -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
 
 let pr_binding = function
-  | [] -> (mt ())
-  | l  -> (str " " ++ prlist_with_sep (fun () -> (str " ")) pr_id l)
+  | [] -> mt ()
+  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
 
-let space_if = function true -> (str " ") | false -> (mt ())
+let space_if = function true -> str " " | false -> mt ()
 
-let sec_space_if = function true -> (spc ()) | false -> (mt ())
+let sec_space_if = function true -> spc () | false -> mt ()
 
 (*s Generic renaming issues. *)
 
@@ -129,10 +125,11 @@ let keywords =
   Idset.empty
 
 let preamble _ used_modules (mldummy,tdummy,tunknown) = 
-  Idset.fold (fun m s -> str "open " ++ pr_id (uppercase_id m) ++ fnl() ++ s)
+  List.fold_right
+    (fun m s -> str "open " ++ pr_id (uppercase_id m) ++ fnl () ++ s)
     used_modules (mt ())
   ++ 
-  (if Idset.is_empty used_modules  then mt () else fnl ())
+  (if used_modules = [] then mt () else fnl ())
   ++
   (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() else mt()) 
   ++
@@ -148,10 +145,14 @@ let preamble _ used_modules (mldummy,tdummy,tunknown) =
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_type_global r = P.pp_global r false (Some (P.globals()))
-let pp_global r env = P.pp_global r false (Some (snd env))
-let pp_global' r = P.pp_global r false None
-let rename_global r = P.rename_global r false 
+let pp_global r = P.pp_global r false None
+
+let pp_global_ctx r env = P.pp_global r false (Some (snd env))
+let pp_global_ctx2 r = P.pp_global r false (Some (P.globals ()))
+
+let pp_global_up r = P.pp_global r true None
+let pp_global_up_ctx r env = P.pp_global r true (Some (snd env))
+
 
 let empty_env () = [], P.globals()
 
@@ -163,11 +164,11 @@ let rec pp_type par vl t =
     | Tmeta _ | Tvar' _ -> assert false
     | Tvar i -> (try pp_tvar (List.nth vl (pred i)) 
 		 with _ -> (str "'a" ++ int i))
-    | Tglob (r,[]) -> pp_type_global r
-    | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_type_global r
+    | Tglob (r,[]) -> pp_global_ctx2 r
+    | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global_ctx2 r
     | Tarr (t1,t2) ->
-	open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
-	pp_rec false t2 ++ close_par par
+	pp_par par 
+	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy -> str "__"
     | Tunknown -> str "__"
   in 
@@ -184,15 +185,10 @@ let expr_needs_par = function
   | MLcase _ -> true
   | _        -> false 
 
-let pp_apply st par args = match args with
-  | [] -> st
-  | _  -> hov 2 (open_par par ++ st ++ spc () ++
-                 prlist_with_sep (fun () -> (spc ())) (fun s -> s) args ++
-                 close_par par) 
 
 let rec pp_expr par env args = 
-  let par' = args <> [] || par in 
-  let apply st = pp_apply st par args in 
+  let par' = args <> [] || par
+  and apply st = pp_apply st par args in 
   function
     | MLrel n -> 
 	let id = get_db_name n env in apply (pr_id id)
@@ -203,36 +199,37 @@ let rec pp_expr par env args =
       	let fl,a' = collect_lams a in
 	let fl,env' = push_vars fl env in
 	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
-	apply (open_par par' ++ st ++ close_par par')
+	apply (pp_par par' st)
     | MLletin (id,a1,a2) ->
+	assert (args=[]); 
 	let i,env' = push_vars [id] env in
-	let par2 = not par' && expr_needs_par a2 in
-	apply 
+	let pp_id = pr_id (List.hd i)
+	and pp_a1 = pp_expr false env [] a1
+	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in 
+	hv 0 
 	  (hv 0 
-	     (hv 0 (open_par par' ++
-		    hov 2 
-		      (str "let " ++ pr_id (List.hd i) ++ str " =" ++ spc ()
-			++ pp_expr false env [] a1) ++ 
-		    spc () ++ str "in") ++ 
-	      spc () ++ hov 0 (pp_expr par2 env' [] a2) ++ close_par par'))
+	     (pp_par par 
+		(hov 2 (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++ 
+		 spc () ++ str "in") ++ 
+	      spc () ++ hov 0 pp_a2))
     | MLglob r when is_proj r && args <> [] ->
 	let record = List.hd args in 
-	pp_apply (record ++ str "." ++ pp_type_global r) par (List.tl args)
+	pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
     | MLglob r -> 
-	apply (pp_global r env )
+	apply (pp_global_ctx r env )
     | MLcons (r,[]) ->
 	assert (args=[]);
+	let cons = pp_global_up_ctx r env in 
 	if Refset.mem r !cons_cofix then 
-	  (open_par par ++ str "lazy " ++ pp_global r env ++ close_par par)
-	else pp_global r env
+	  pp_par par (str "lazy " ++ cons)
+	else cons 
     | MLcons (r,args') ->
 	assert (args=[]);
+	let cons = pp_global_up_ctx r env
+	and tuple = pp_tuple (pp_expr true env []) args' in 
 	if Refset.mem r !cons_cofix then 
-	  (open_par par ++ str "lazy (" ++ pp_global r env ++ spc () ++
-	   pp_tuple (pp_expr true env []) args' ++ str ")" ++ close_par par)
-	else
-	  (open_par par ++ pp_global r env ++ spc () ++
-	   pp_tuple (pp_expr true env []) args' ++ close_par par)
+	  pp_par par (str "lazy (" ++ cons ++ spc () ++ tuple ++ str ")")
+	else pp_par par (cons ++ spc () ++ tuple)
     | MLcase (t,[|(r,_,_) as x|])->
 	let expr = if Refset.mem r !cons_cofix then 
 	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
@@ -242,39 +239,36 @@ let rec pp_expr par env args =
 	let s1,s2 = pp_one_pat env x in 
 	apply 
 	  (hv 0 
-	     (hv 0 (open_par par' ++ 
-		    hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) ++ 
+	     (hv 0 
+		(pp_par par' 
+		   (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) ++ 
 		    spc () ++ str "in") ++ 
-	      spc () ++ hov 0 s2 ++ close_par par'))
+		 spc () ++ hov 0 s2)))
     | MLcase (t, pv) ->
 	let r,_,_ = pv.(0) in 
-	let expr = if Refset.mem r !cons_cofix then 
-	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
-	else 
-	  (pp_expr false env [] t) 	
-	in apply
-      	     (open_par par' ++
-      	      v 0 (str "match " ++ expr ++ str " with" ++
-		   fnl () ++ str "  | " ++ pp_pat env pv) ++
-	      close_par par')
+	let expr = 
+	  if Refset.mem r !cons_cofix then 
+	    (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
+	  else pp_expr false env [] t in 
+	apply
+      	  (pp_par par' 
+      	     (v 0 (str "match " ++ expr ++ str " with" ++
+		   fnl () ++ str "  | " ++ pp_pat env pv)))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
     | MLexn s -> 
 	(* An [MLexn] may be applied, but I don't really care. *)
-	(open_par par ++ str "assert false" ++ spc () ++ 
-	 str ("(* "^s^" *)") ++ close_par par)
+	pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
     | MLdummy ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLcast (a,t) ->
-	apply 
-	  (open_par true ++ pp_expr true env [] a ++ spc () ++ str ":" ++ 
-	 spc () ++ pp_type true [] t ++ close_par true)
+	apply (pp_par true 
+		 (pp_expr true env [] a ++ spc () ++ str ":" ++ 
+		  spc () ++ pp_type true [] t))
     | MLmagic a ->
-	let args' = pp_expr true env [] a :: args in 
-	hov 2 (open_par par ++ str "Obj.magic" ++ spc () ++
-               prlist_with_sep (fun () -> (spc ())) (fun s -> s) args' ++
-	       close_par par)
+	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args) 
+
 
 and pp_one_pat env (r,ids,t) = 
   let ids,env' = push_vars (List.rev ids) env in
@@ -282,7 +276,7 @@ and pp_one_pat env (r,ids,t) =
   let args = 
     if ids = [] then (mt ()) 
     else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in 
-  (pp_global r env ++ args), (pp_expr par env' [] t)
+  (pp_global_up_ctx r env ++ args), (pp_expr par env' [] t)
   
 and pp_pat env pv = 
   prvect_with_sep (fun () -> (fnl () ++ str "  | ")) 
@@ -318,36 +312,28 @@ and pp_function env f t =
     and passed here just for convenience. *)
 
 and pp_fix par env i (ids,bl) args =
-  open_par par ++ 
-  v 0 (str "let rec " ++
-       prvect_with_sep
-      	 (fun () -> (fnl () ++ str "and "))
-	 (fun (fi,ti) -> pp_function env (pr_id fi) ti)
-	 (array_map2 (fun id b -> (id,b)) ids bl) ++
-       fnl () ++
-       hov 2 (str "in " ++ pr_id ids.(i) ++
-	      if args <> [] then
-		(str " " ++ 
-		 prlist_with_sep (fun () -> (str " "))
-		   (fun s -> s) args)
-	      else mt ())) ++
-  close_par par
+  pp_par par 
+    (v 0 (str "let rec " ++
+	  prvect_with_sep
+      	    (fun () -> fnl () ++ str "and ")
+	    (fun (fi,ti) -> pp_function env (pr_id fi) ti)
+	    (array_map2 (fun id b -> (id,b)) ids bl) ++
+	  fnl () ++
+	  hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
 
 let pp_val e typ = 
   str "(** val " ++ e ++ str " : " ++ pp_type false [] typ ++ 
-  str " **)"  ++ fnl() ++ fnl()
+  str " **)"  ++ fnl () ++ fnl ()
 
 (*s Pretty-printing of [Dfix] *)
 
-let pp_Dfix env (ids,bl,typs) = 
+let pp_Dfix env (p,c,t) = 
   let init = 
-    pp_val (pr_id ids.(0)) (typs.(0)) ++
-    str "let rec " ++ pp_function env (pr_id ids.(0)) bl.(0) ++ fnl()
+    pp_val p.(0) t.(0) ++ str "let rec " ++ pp_function env p.(0) c.(0) ++ fnl ()
   in
-  iterate_for 1 (Array.length ids - 1) 
-    (fun i acc -> 
-       acc ++ fnl() ++ pp_val (pr_id ids.(i)) (typs.(i)) ++
-       str "and " ++ pp_function env (pr_id ids.(i)) bl.(i) ++ fnl())
+  iterate_for 1 (Array.length p - 1) 
+    (fun i acc -> acc ++ fnl () ++ 
+       pp_val p.(i) t.(i) ++ str "and " ++ pp_function env p.(i) c.(i) ++ fnl ())
     init 
 	
 (*s Pretty-printing of inductive types declaration. *)
@@ -357,8 +343,8 @@ let pp_parameters l =
 
 let pp_one_ind prefix (pl,name,cl) =
   let pl = rename_tvars keywords pl in
-  let pp_constructor (id,l) =
-    (pp_global' id ++
+  let pp_constructor (r,l) =
+    (pp_global_up r ++
      match l with
        | [] -> (mt ()) 
        | _  -> (str " of " ++
@@ -366,7 +352,7 @@ let pp_one_ind prefix (pl,name,cl) =
 		  (fun () -> (spc () ++ str "* ")) 
 		  (pp_type true pl) l))
   in
-  (pp_parameters pl ++ str prefix ++ pp_type_global name ++ str " =" ++ 
+  (pp_parameters pl ++ str prefix ++ pp_global name ++ str " =" ++ 
    if cl = [] then str " unit (* empty inductive *)" 
    else (fnl () ++
 	 v 0 (str "  | " ++
@@ -374,28 +360,28 @@ let pp_one_ind prefix (pl,name,cl) =
                 (fun c -> hov 2 (pp_constructor c)) cl)))
 
 let pp_ind il =
-  (str "type " ++
-   prlist_with_sep (fun () -> (fnl () ++ str "and ")) (pp_one_ind "") il
-   ++ fnl ())
+  str "type " ++
+  prlist_with_sep (fun () -> fnl () ++ str "and ") (pp_one_ind "") il
+  ++ fnl ()
 
 let pp_record ip pl l = 
   let pl = rename_tvars keywords pl in 
-  (str "type " ++ pp_parameters pl ++ pp_type_global (IndRef ip) ++ str " = { "++
-   hov 0 (prlist_with_sep (fun () -> (str ";" ++ spc ())) 
-	    (fun (r,t) -> pp_type_global r ++ str " : " ++ pp_type true pl t) l)
-   ++ str " }") 
+  str "type " ++ pp_parameters pl ++ pp_global (IndRef ip) ++ str " = { "++
+  hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) 
+	   (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l)
+  ++ str " }" ++ fnl () 
 
 let pp_coind_preamble (pl,name,_) = 
   let pl = rename_tvars keywords pl in
-  (pp_parameters pl ++ pp_type_global name ++ str " = " ++ 
-    pp_parameters pl ++ str "__" ++ pp_type_global name ++ str " Lazy.t")
+  pp_parameters pl ++ pp_global name ++ str " = " ++ 
+  pp_parameters pl ++ str "__" ++ pp_global name ++ str " Lazy.t"
 
 let pp_coind il = 
-  (str "type " ++ 
-   prlist_with_sep (fun () -> (fnl () ++ str "and ")) pp_coind_preamble il ++
-   fnl () ++ str "and " ++ 
-   prlist_with_sep (fun () -> (fnl () ++ str "and ")) (pp_one_ind "__") il ++
-   fnl ())
+  str "type " ++ 
+  prlist_with_sep (fun () -> fnl () ++ str "and ") pp_coind_preamble il ++
+  fnl () ++ str "and " ++ 
+  prlist_with_sep (fun () -> fnl () ++ str "and ") (pp_one_ind "__") il ++
+  fnl ()
 
 (*s Pretty-printing of a declaration. *)
 
@@ -416,21 +402,21 @@ let pp_decl = function
   | Dtype (r, l, t) ->
       let l = rename_tvars keywords l in 
       hov 0 (str "type" ++ spc () ++ pp_parameters l ++ 
-	       pp_type_global r ++ spc () ++ str "=" ++ spc () ++ 
+	       pp_global r ++ spc () ++ str "=" ++ spc () ++ 
 	       pp_type false l t ++ fnl ())
   | Dfix (rv, defs, typs) ->
-      let ids = Array.map rename_global rv in 
-      let env = List.rev (Array.to_list ids), P.globals() in
-      hov 0 (pp_Dfix env (ids,defs,typs))
+      (* We compute renamings of [rv] before asking [empty_env ()]... *)
+      let ppv = Array.map pp_global rv in 
+      hov 0 (pp_Dfix (empty_env ()) (ppv,defs,typs))
   | Dterm (r, a, t) ->
-      let e = pp_global' r in 
+      let e = pp_global r in 
       (pp_val e t ++ 
        hov 0 (str "let " ++ pp_function (empty_env ()) e a ++ fnl ()))
   | DcustomTerm (r,s) -> 
-      hov 0 (str "let " ++ pp_global' r ++ 
+      hov 0 (str "let " ++ pp_global r ++ 
 	     str " =" ++ spc () ++ str s ++ fnl ())
   | DcustomType (r,s) -> 
-      hov 0 (str "type " ++ pp_type_global r ++ str " = " ++ str s ++ fnl ())
+      hov 0 (str "type " ++ pp_global r ++ str " = " ++ str s ++ fnl ())
 
 end
 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index bda89d9372..1984472967 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -20,9 +20,9 @@ open Table
 val current_module : identifier option ref
 val cons_cofix : Refset.t ref
 
-val open_par : bool -> std_ppcmds
-val close_par : bool -> std_ppcmds
+val pp_par : bool -> std_ppcmds -> std_ppcmds
 val pp_abst : identifier list -> std_ppcmds
+val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds 
 val pr_binding : identifier list -> std_ppcmds
 
 val rename_id : identifier -> Idset.t -> identifier
@@ -39,7 +39,8 @@ val get_db_name : int -> env -> identifier
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
+val preamble : 
+  extraction_params -> identifier list -> bool * bool * bool -> std_ppcmds
 
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 40d0ec5e2c..55a30185da 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -30,7 +30,6 @@ let keywords =
       "apply"; "car"; "cdr"; 
       "error"; "delay"; "force"; "_"; "__"] 
     Idset.empty
-    
 
 let preamble _ _ (mldummy,_,_) = 
   (if mldummy then 
@@ -38,7 +37,7 @@ let preamble _ _ (mldummy,_,_) =
      ++ fnl () ++ fnl()
    else mt ())
 
-let paren st = str "(" ++ st ++ str ")"
+let paren = pp_par true
 
 let pp_abst st = function 
   | [] -> assert false
@@ -50,21 +49,17 @@ let pp_abst st = function
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_global r env = P.pp_global r false (Some (snd env))
-let pp_global' r = P.pp_global r false None
-
-let rename_global r = P.rename_global r false 
+let pp_global r = P.pp_global r false None
+let pp_global_ctx r env = P.pp_global r false (Some (snd env))
+let pp_global_up r = P.pp_global r true None
+let pp_global_up_ctx r env = P.pp_global r true (Some (snd env))
 
 let empty_env () = [], P.globals()
 
-let rec apply st = function 
-  | [] -> st 
-  | a :: args -> apply (paren (st ++ spc () ++ a)) args 
-
 (*s Pretty-printing of expressions.  *)
 
 let rec pp_expr env args = 
-  let apply st = apply st args in 
+  let apply st = pp_apply st true args in 
   function
     | MLrel n -> 
 	let id = get_db_name n env in apply (pr_id id)
@@ -87,12 +82,12 @@ let rec pp_expr env args =
 			 (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) 
 		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
     | MLglob r -> 
-	apply (pp_global r env)
+	apply (pp_global_ctx r env)
     | MLcons (r,args') ->
 	assert (args=[]);
 	let st = 
 	  str "`" ++ 
-	  paren (pp_global r env ++ 
+	  paren (pp_global_up_ctx r env ++ 
 		 (if args' = [] then mt () else (spc () ++ str ",")) ++
 		 prlist_with_sep 
 		   (fun () -> spc () ++ str ",") 
@@ -130,7 +125,7 @@ and pp_one_pat env (r,ids,t) =
     if ids = [] then mt () 
     else (str " " ++ prlist_with_sep spc pp_arg (List.rev ids))
   in 
-  (pp_global r env ++ args), (pp_expr env' [] t)
+  (pp_global_up_ctx r env ++ args), (pp_expr env' [] t)
   
 and pp_pat env pv = 
   prvect_with_sep fnl  
@@ -148,7 +143,7 @@ and pp_fix env j (ids,bl) args =
 		  (fun (fi,ti) -> paren ((pr_id fi) ++ (pp_expr env [] ti)))
 		  (array_map2 (fun id b -> (id,b)) ids bl)) ++
 	     fnl () ++
-      	     hov 2 (apply (pr_id (ids.(j))) args))))
+      	     hov 2 (pp_apply (pr_id (ids.(j))) true args))))
 
 (*s Pretty-printing of a declaration. *)
 
@@ -157,21 +152,19 @@ let pp_decl = function
   | Dtype _ -> mt () 
   | DcustomType _ -> mt ()
   | Dfix (rv, defs,_) ->
-      let ids = Array.map rename_global rv in 
-      let env = List.rev (Array.to_list ids), P.globals() in
-      prvect_with_sep 
-	fnl 
-	(fun (fi,ti) -> 
+      let ppv = Array.map pp_global rv in 
+      prvect_with_sep fnl 
+	(fun (pi,ti) -> 
 	   hov 2 
-	     (paren (str "define " ++ pr_id fi ++ spc () ++ 
-		     (pp_expr env [] ti)) 
+	     (paren (str "define " ++ pi ++ spc () ++ 
+		     (pp_expr (empty_env ()) [] ti)) 
 	      ++ fnl ()))
-	(array_map2 (fun id b -> (id,b)) ids defs)
+	(array_map2 (fun p b -> (p,b)) ppv defs)
   | Dterm (r, a, _) ->
-      hov 2 (paren (str "define " ++ (pp_global' r) ++ spc () ++
+      hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
 		    pp_expr (empty_env ()) [] a)) ++ fnl ()  
   | DcustomTerm (r,s) -> 
-      hov 2 (paren (str "define " ++ pp_global' r ++ spc () ++ str s) ++ fnl ())
+      hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ str s) ++ fnl ())
 
 end
 
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index 51fac4fb72..f39afd34f0 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -17,7 +17,8 @@ open Nametab
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
+val preamble : 
+  extraction_params -> identifier list -> bool * bool * bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp