typo de parenthèsage + suppression de string (= str maintenant)

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

4 files changed, 24 insertions, 27 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 9467986ef8..80f62eb3c0 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -124,10 +124,10 @@ module MonoParams = struct
 	   | _ -> rename_global_id (lowercase_id id))
       
   let pp_type_global r = 
-    string (check_ml r (string_of_id (rename_type_global r)))
+    str (check_ml r (string_of_id (rename_type_global r)))
       
   let pp_global r = 
-    string (check_ml r (string_of_id (rename_global r)))
+    str (check_ml r (string_of_id (rename_global r)))
       
 end
 
@@ -168,11 +168,11 @@ module ModularParams = struct
 	   | _ -> rename_global_id r id (lowercase_id id) "coq_")
 
   let pp_type_global r = 
-    string 
+    str 
       (check_ml r ((module_option r)^(string_of_id (rename_type_global r))))
 
   let pp_global r = 
-    string 
+    str
       (check_ml r ((module_option r)^(string_of_id (rename_global r))))
 
 end
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 499503f171..fcba0fcb55 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -75,11 +75,11 @@ let rec pp_type par t =
     | Tglob r -> 
 	pp_type_global r
     | Texn s -> 
-	(string ("() -- " ^ s) ++ fnl ())
+	(str ("() -- " ^ s) ++ fnl ())
     | Tprop ->
-	string "Prop"
+	str "Prop"
     | Tarity ->
-	string "Arity"
+	str "Arity"
   in 
   hov 0 (pp_rec par t)
 
@@ -148,9 +148,9 @@ let rec pp_expr par env args =
     | MLexn s -> 
 	(open_par par ++ str "error" ++ spc () ++ qs s ++ close_par par)
     | MLprop ->
-	string "prop"
+	str "prop"
     | MLarity ->
-	string "arity"
+	str "arity"
     | MLcast (a,t) ->
 	(open_par true ++ pp_expr false env args a ++ spc () ++ str "::" ++ spc () ++ 
 	   pp_type false t ++ close_par true)
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 36ccff88d1..6705b8a4b1 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -29,17 +29,15 @@ let rec collapse_type_app = function
   | (Tapp l1) :: l2 -> collapse_type_app (l1 @ l2)
   | l -> l
 
-let string s = (str s)
+let open_par = function true -> str "(" | false -> (mt ())
 
-let open_par = function true -> string "(" | false -> (mt ())
-
-let close_par = function true -> string ")" | false -> (mt ())
+let close_par = function true -> str ")" | false -> (mt ())
 
 let pp_tvar id = 
   let s = string_of_id id in 
   if String.length s < 2 || s.[1]<>'\'' 
-  then string ("'"^s)
-  else string ("' "^s)
+  then str ("'"^s)
+  else str ("' "^s)
 
 let pp_tuple f = function
   | [] -> (mt ())
@@ -149,11 +147,11 @@ let rec pp_type par t =
     | Tglob r -> 
 	pp_type_global r
     | Texn s -> 
-	string ("unit (* " ^ s ^ " *)")
+	str ("unit (* " ^ s ^ " *)")
     | Tprop ->
-	string "prop"
+	str "prop"
     | Tarity ->
-	string "arity"
+	str "arity"
   in 
   hov 0 (pp_rec par t)
 
@@ -227,9 +225,9 @@ let rec pp_expr par env args =
 	(open_par par ++ str "assert false" ++ spc () ++ 
 	   str ("(* "^s^" *)") ++ close_par par)
     | MLprop ->
-	string "prop"
+	str "prop"
     | MLarity ->
-	string "arity"
+	str "arity"
     | MLcast (a,t) ->
 	(open_par true ++ pp_expr false env args a ++ spc () ++ str ":" ++ spc () ++ 
 	   pp_type false t ++ close_par true)
@@ -240,14 +238,14 @@ let rec pp_expr par env args =
 and pp_one_pat s env (r,ids,t) = 
   let ids,env' = push_vars (List.rev ids) env in
   let par = expr_needs_par t in
-  (pp_global r ++ 
-     if ids = [] then (mt ()) 
-     else (str " " ++ pp_boxed_tuple pr_id (List.rev ids)) ++
-     s ++ spc () ++ pp_expr par env' [] t)
+  let args = 
+    if ids = [] then (mt ()) 
+    else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in 
+  pp_global r ++ args ++ s ++ spc () ++ pp_expr par env' [] t
   
 and pp_pat env pv = 
-  (prvect_with_sep (fun () -> (fnl () ++ str "| ")) 
-       (fun x -> hov 2 (pp_one_pat (string " ->") env x)) pv)
+  prvect_with_sep (fun () -> (fnl () ++ str "| ")) 
+    (fun x -> hov 2 (pp_one_pat (str " ->") env x)) pv
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index e9faa1a0a9..3c39348367 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -20,7 +20,6 @@ val current_module : identifier option ref
 
 val collapse_type_app : ml_type list -> ml_type list
 
-val string : string -> std_ppcmds
 val open_par : bool -> std_ppcmds
 val close_par : bool -> std_ppcmds
 val pp_abst : identifier list -> std_ppcmds