compat ocaml 3.03

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

7 files changed, 244 insertions, 244 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 9b111bbf4..9467986ef 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -45,8 +45,8 @@ let long_module r =
 	try 
 	  dirpath_prefix d 
 	with _ -> errorlabstrm "long_module_message"
-	[< 'sTR "Can't find the module of"; 'sPC; 
-	   Printer.pr_global r >]
+	(str "Can't find the module of" ++ spc () ++ 
+	   Printer.pr_global r)
       in check_module d' 
   in check_module (dirpath (sp_of_r r))
 
@@ -210,10 +210,10 @@ let extract_to_file f prm decls =
   in
   let cout = open_out f in
   let ft = Pp_control.with_output_to cout in
-  if decls <> [] then pP_with ft (hV 0 (preamble prm));
+  if decls <> [] then pp_with ft (hv 0 (preamble prm));
   begin 
     try
-      List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
+      List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
     with e ->
       pp_flush_with ft (); close_out cout; raise e
   end;
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 8ce82a45b..ce367c1c2 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -32,16 +32,16 @@ let module_of_id m =
     locate_loaded_library (make_short_qualid m) 
   with Not_found ->  
     errorlabstrm "module_message"
-      [< 'sTR "Module"; 'sPC;pr_id m; 'sPC; 'sTR "not found." >] 
+      (str "Module" ++ spc () ++ pr_id m ++ spc () ++ str "not found.") 
 
 (*s Module name clash verification. *)
 
 let clash_error sn n1 n2 = 
   errorlabstrm "clash_module_message"
-    [< 'sTR ("There are two Coq modules with ML name " ^ sn ^" :"); 
-       'fNL ; 'sTR ("  "^(string_of_dirpath n1)) ; 
-       'fNL ; 'sTR ("  "^(string_of_dirpath n2)) ; 
-       'fNL ; 'sTR "This is not allowed in ML. Please do some renaming first." >]
+    (str ("There are two Coq modules with ML name " ^ sn ^" :") ++ 
+     fnl () ++ str ("  "^(string_of_dirpath n1)) ++ 
+     fnl () ++ str ("  "^(string_of_dirpath n2)) ++ 
+     fnl () ++ str "This is not allowed in ML. Please do some renaming first.")
     
 let check_r m sm r = 
   let rm = String.capitalize (string_of_id (short_module r)) in 
@@ -205,8 +205,8 @@ let local_optimize refs =
   optimize prm (decl_of_refs refs)
 
 let print_user_extract r = 
-  mSGNL [< 'sTR "User defined extraction:"; 
-	   'sPC; 'sTR (find_ml_extraction r) ; 'fNL>]
+  msgnl (str "User defined extraction:" ++ 
+	   spc () ++ str (find_ml_extraction r) ++ fnl ())
 
 let decl_in_r r0 = function 
   | Dglob (r,_) -> r = r0
@@ -220,7 +220,7 @@ let extract_reference r =
     print_user_extract r 
   else
     let d = list_last (local_optimize [r]) in
-    mSGNL (ToplevelPp.pp_decl 
+    msgnl (ToplevelPp.pp_decl 
 	     (if (decl_in_r r d) || d = Dtype([],true) || d = Dtype([],false) 
 	     then d 
 	     else List.find (decl_in_r r) (local_optimize [r])))
@@ -239,8 +239,8 @@ let _ =
 		(* Otherwise, output the ML type or expression *)
 		| _ ->
 		    match extract_constr (Global.env()) c with
-		      | Emltype (t,_,_) -> mSGNL (ToplevelPp.pp_type t)
-		      | Emlterm a -> mSGNL (ToplevelPp.pp_ast (normalize a)))
+		      | Emltype (t,_,_) -> msgnl (ToplevelPp.pp_type t)
+		      | Emlterm a -> msgnl (ToplevelPp.pp_ast (normalize a)))
        | _ -> assert false)
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
@@ -255,7 +255,7 @@ let _ =
        let rl = List.filter (fun x -> not (is_ml_extraction x)) rl in 
        let dl = local_optimize rl in
        List.iter print_user_extract ml_rl ;
-       List.iter (fun d -> mSGNL (ToplevelPp.pp_decl d)) dl)
+       List.iter (fun d -> msgnl (ToplevelPp.pp_decl d)) dl)
 
 (*s Extraction to a file (necessarily recursive). 
     The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn].
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 132367de9..b9a43fd04 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -244,12 +244,12 @@ let decompose_lam_eta n env c =
 
 let axiom_message sp =
   errorlabstrm "axiom_message"
-    [< 'sTR "You must specify an extraction for axiom"; 'sPC; 
-       pr_sp sp; 'sPC; 'sTR "first" >]
+    (str "You must specify an extraction for axiom" ++ spc () ++ 
+       pr_sp sp ++ spc () ++ str "first")
 
 let section_message () = 
   errorlabstrm "section_message"
-    [< 'sTR "You can't extract within a section. Close it and try again" >]
+    (str "You can't extract within a section. Close it and try again")
 
 (*s Tables to keep the extraction of inductive types and constructors. *)
 
@@ -421,8 +421,8 @@ and extract_type_app env (r,sc,vlc) vl args =
   let args = if diff > 0 then begin
     (* This can (normally) only happen when r is a flexible type. 
        We discard the remaining arguments *)
-    (*i    wARN (hOV 0 [< 'sTR ("Discarding " ^
-		 (string_of_int diff) ^ " type(s) argument(s).") >]); i*)
+    (*i    wARN (hov 0 (str ("Discarding " ^
+		 (string_of_int diff) ^ " type(s) argument(s)."))); i*)
     list_firstn (List.length sc) args
   end else args in
   let nargs = List.length args in
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 8d5cf6ebe..499503f17 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -36,11 +36,11 @@ let preamble prm =
     | None -> "Main" 
     | Some m -> String.capitalize (string_of_id m) 
   in 
-  [< 'sTR "module "; 'sTR m; 'sTR " where"; 'fNL; 'fNL;
-     'sTR "type Prop = ()"; 'fNL;
-     'sTR "prop = ()"; 'fNL; 'fNL;
-     'sTR "type Arity = ()"; 'fNL;
-     'sTR "arity = ()"; 'fNL; 'fNL >]
+  (str "module " ++ str m ++ str " where" ++ fnl () ++ fnl () ++
+     str "type Prop = ()" ++ fnl () ++
+     str "prop = ()" ++ fnl () ++ fnl () ++
+     str "type Arity = ()" ++ fnl () ++
+     str "arity = ()" ++ fnl () ++ fnl ())
 
 (*s The pretty-printing functor. *)
 
@@ -65,23 +65,23 @@ let rec pp_type par t =
 	   | [] -> assert false
 	   | [t] -> pp_rec par t
 	   | t::l -> 
-	       [< open_par par;
-		  pp_rec false t; 'sPC;
-		  prlist_with_sep (fun () -> [< 'sPC >]) (pp_type true) l; 
-		  close_par par >])
+	       (open_par par ++
+		  pp_rec false t ++ spc () ++
+		  prlist_with_sep (fun () -> (spc ())) (pp_type true) l ++ 
+		  close_par par))
     | Tarr (t1,t2) ->
-	[< open_par par; pp_rec true t1; 'sPC; 'sTR "->"; 'sPC; 
-	   pp_rec false t2; close_par par >]
+	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
+	   pp_rec false t2 ++ close_par par)
     | Tglob r -> 
 	pp_type_global r
     | Texn s -> 
-	[< string ("() -- " ^ s) ; 'fNL >]
+	(string ("() -- " ^ s) ++ fnl ())
     | Tprop ->
 	string "Prop"
     | Tarity ->
 	string "Arity"
   in 
-  hOV 0 (pp_rec par t)
+  hov 0 (pp_rec par t)
 
 (*s Pretty-printing of expressions. [par] indicates whether
     parentheses are needed or not. [env] is the list of names for the
@@ -96,9 +96,9 @@ let expr_needs_par = function
 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 >] 
+    | _  -> hov 2 (open_par par ++ st ++ spc () ++
+                     prlist_with_sep (fun () -> (spc ())) (fun s -> s) args ++
+                     close_par par) 
   in
   function
     | MLrel n -> 
@@ -109,155 +109,155 @@ let rec pp_expr par env args =
     | MLlam _ as a -> 
       	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
+	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
 	if args = [] then
-          [< open_par par; st; close_par par >]
+          (open_par par ++ st ++ close_par par)
         else
-          apply [< 'sTR "("; st; 'sTR ")" >]
+          apply (str "(" ++ st ++ str ")")
     | MLletin (id,a1,a2) ->
 	let id',env' = push_vars [id] env in
 	let par' = par || args <> [] in
 	let par2 = not par' && expr_needs_par a2 in
 	apply 
-	  (hOV 0 [< open_par par';
-		    hOV 2 [< 'sTR "let "; pr_id (List.hd id'); 'sTR " ="; 'sPC;
-			     pp_expr false env [] a1; 'sPC; 'sTR "in" >];
-		    'sPC;
-		    pp_expr par2 env' [] a2;
-		    close_par par' >])
+	  (hov 0 (open_par par' ++
+		    hov 2 (str "let " ++ pr_id (List.hd id') ++ str " =" ++ spc () ++
+			     pp_expr false env [] a1 ++ spc () ++ str "in") ++
+		    spc () ++
+		    pp_expr par2 env' [] a2 ++
+		    close_par par'))
     | MLglob r -> 
 	apply (pp_global r)
     | MLcons (r,[]) ->
 	pp_global r
     | MLcons (r,[a]) ->
-	[< open_par par; pp_global r; 'sPC;
-	   pp_expr true env [] a; close_par par >]
+	(open_par par ++ pp_global r ++ spc () ++
+	   pp_expr true env [] a ++ close_par par)
     | MLcons (r,args') ->
-	[< open_par par; pp_global r; 'sPC;
-	   prlist_with_sep (fun () -> [< 'sPC >]) (pp_expr true env []) args';
-	   close_par par >]
+	(open_par par ++ pp_global r ++ spc () ++
+	   prlist_with_sep (fun () -> (spc ())) (pp_expr true env []) args' ++
+	   close_par par)
     | 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 >]
+      	  (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)
     | 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
-    | MLexn str -> 
-	[< open_par par; 'sTR "error"; 'sPC; 'qS str; close_par par >]
+    | MLexn s -> 
+	(open_par par ++ str "error" ++ spc () ++ qs s ++ close_par par)
     | MLprop ->
 	string "prop"
     | MLarity ->
 	string "arity"
     | MLcast (a,t) ->
-	[< open_par true; pp_expr false env args a; 'sPC; 'sTR "::"; 'sPC; 
-	   pp_type false t; close_par true >]
+	(open_par true ++ pp_expr false env args a ++ spc () ++ str "::" ++ spc () ++ 
+	   pp_type false t ++ close_par true)
     | MLmagic a ->
-	[< open_par true; 'sTR "Obj.magic"; 'sPC; 
-	   pp_expr false env args a; close_par true >]
+	(open_par true ++ str "Obj.magic" ++ spc () ++ 
+	   pp_expr false env args a ++ close_par true)
 
 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;
+    hov 2 (pp_global name ++
 	     begin match ids with 
-	       | [] -> [< >]
-	       | _  -> [< 'sTR " "; 
+	       | [] -> (mt ())
+	       | _  -> (str " " ++ 
 			  prlist_with_sep 
-			    (fun () -> [< 'sPC >]) pr_id (List.rev ids) >]
-	     end;
-	     'sTR " ->"; 'sPC; pp_expr par env' [] t >]
+			    (fun () -> (spc ())) pr_id (List.rev ids))
+	     end ++
+	     str " ->" ++ spc () ++ pp_expr par env' [] t)
   in 
-  [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "  " >]) pp_one_pat pv >]
+  (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 [< 'sTR "let { " ;
+  (open_par par ++ 
+     v 0 (str "let { " ++
 	    prvect_with_sep
-      	      (fun () -> [< 'sTR "; "; 'fNL >])
+      	      (fun () -> (str "; " ++ fnl ()))
 	      (fun (fi,ti) -> pp_function env (pr_id fi) ti)
-	      (array_map2 (fun id b -> (id,b)) ids bl);
-	    'sTR " }";'fNL;
+	      (array_map2 (fun id b -> (id,b)) ids bl) ++
+	    str " }" ++fnl () ++
 	    match in_p with
 	      | Some j -> 
-      		  hOV 2 [< 'sTR "in "; pr_id ids.(j);
+      		  hov 2 (str "in " ++ pr_id ids.(j) ++
 			   if args <> [] then
-			     [< 'sTR " "; 
-				prlist_with_sep (fun () -> [<'sTR " ">])
-				  (fun s -> s) args >]
+			     (str " " ++ 
+				prlist_with_sep (fun () -> (str " "))
+				  (fun s -> s) args)
 			   else
-			     [< >] >]
+			     (mt ()))
 	      | None -> 
-		  [< >] >];
-     close_par par >]
+		  (mt ())) ++
+     close_par par)
 
 and pp_function env f t =
   let bl,t' = collect_lams t in
   let bl,env' = push_vars bl env in
-  [< f; pr_binding (List.rev bl);
-     'sTR " ="; 'fNL; 'sTR "  ";
-     hOV 2 (pp_expr false env' [] t') >]
+  (f ++ pr_binding (List.rev bl) ++
+     str " =" ++ fnl () ++ str "  " ++
+     hov 2 (pp_expr false env' [] t'))
 	
-let pp_ast a = hOV 0 (pp_expr false (empty_env ()) [] a)
+let pp_ast a = hov 0 (pp_expr false (empty_env ()) [] a)
 
 (*s Pretty-printing of inductive types declaration. *)
 
 let pp_one_inductive (pl,name,cl) =
   let pp_constructor (id,l) =
-    [< pp_global id;
+    (pp_global id ++
        match l with
-         | [] -> [< >] 
-	 | _  -> [< 'sTR " " ;
+         | [] -> (mt ()) 
+	 | _  -> (str " " ++
       	       	    prlist_with_sep 
-		      (fun () -> [< 'sTR " " >]) (pp_type true) l >] >]
+		      (fun () -> (str " ")) (pp_type true) l))
   in
-  [< 'sTR (if cl = [] then "type " else "data "); 
-     pp_type_global name; 'sTR " ";
-     prlist_with_sep (fun () -> [< 'sTR " " >]) pr_lower_id pl;
-     if pl = [] then [< >] else [< 'sTR " " >];
-     [< v 0 [< 'sTR "= ";
-	       prlist_with_sep (fun () -> [< 'fNL; 'sTR "  | " >])
-                 pp_constructor cl >] >] >]
+  (str (if cl = [] then "type " else "data ") ++ 
+     pp_type_global name ++ str " " ++
+     prlist_with_sep (fun () -> (str " ")) pr_lower_id pl ++
+     if pl = [] then (mt ()) else (str " ") ++
+     (v 0 (str "= " ++
+	       prlist_with_sep (fun () -> (fnl () ++ str "  | "))
+                 pp_constructor cl)))
 
 let pp_inductive il =
-  [< prlist_with_sep (fun () -> [< 'fNL >]) pp_one_inductive il; 'fNL >]
+  (prlist_with_sep (fun () -> (fnl ())) pp_one_inductive il ++ fnl ())
 
 (*s Pretty-printing of a declaration. *)
 
 let pp_decl = function
   | Dtype ([], _) -> 
-      [< >]
+      (mt ())
   | Dtype (i, _) -> 
-      hOV 0 (pp_inductive i)
+      hov 0 (pp_inductive i)
   | Dabbrev (r, l, t) ->
-      hOV 0 [< 'sTR "type "; pp_type_global r; 'sPC; 
-	       prlist_with_sep (fun () -> [< 'sTR " " >]) pr_lower_id l;
-	       if l <> [] then [< 'sTR " " >] else [< >]; 'sTR "="; 'sPC;
-	       pp_type false t; 'fNL >]
+      hov 0 (str "type " ++ pp_type_global r ++ spc () ++ 
+	       prlist_with_sep (fun () -> (str " ")) pr_lower_id l ++
+	       if l <> [] then (str " ") else (mt ()) ++ str "=" ++ spc () ++
+	       pp_type false t ++ fnl ())
   | Dglob (r, MLfix (i,ids,defs)) ->
       let env = empty_env () in
       let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-      [< prlist_with_sep (fun () -> [< 'fNL >])
+      (prlist_with_sep (fun () -> (fnl ()))
 	   (fun (fi,ti) -> pp_function env' (pr_id fi) ti)
-	   (List.combine (List.rev ids') (Array.to_list defs));
-	 'fNL;
+	   (List.combine (List.rev ids') (Array.to_list defs)) ++
+	 fnl () ++
 	 let id = rename_global r in
 	 let idi = List.nth (List.rev ids') i in
 	 if id <> idi then
-	   [< 'fNL; pr_id id; 'sTR " = "; pr_id idi; 'fNL >]
+	   (fnl () ++ pr_id id ++ str " = " ++ pr_id idi ++ fnl ())
 	 else
-	   [< >] >]
+	   (mt ()))
   | Dglob (r, a) ->
-      hOV 0 [< pp_function (empty_env ()) (pp_global r) a; 'fNL >]
+      hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl ())
   | Dcustom (r,s) -> 
-      hOV 0  [< pp_global r; 'sTR " ="; 
-		'sPC; 'sTR s; 'fNL  >]
+      hov 0  (pp_global r ++ str " =" ++ 
+		spc () ++ str s ++ fnl ())
 
 let pp_type = pp_type false
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 32ad5053b..53408461f 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -581,15 +581,15 @@ let subst_glob_decl r m = function
   | d -> d
 
 let warning_expansion r = 
-  wARN (hOV 0 [< 'sTR "The constant"; 'sPC;
-		 Printer.pr_global r; 
-(*i    'sTR (" of size "^ (string_of_int (ml_size t))); i*)
-    'sPC; 'sTR "is expanded." >])
+  warn (hov 0 (str "The constant" ++ spc () ++
+		 Printer.pr_global r ++ 
+(*i    str (" of size "^ (string_of_int (ml_size t))) ++ i*)
+    spc () ++ str "is expanded."))
 
 let warning_expansion_must r = 
-  wARN (hOV 0 [< 'sTR "The constant"; 'sPC;
-		 Printer.pr_global r; 
-    'sPC; 'sTR "must be expanded." >])
+  warn (hov 0 (str "The constant" ++ spc () ++
+		 Printer.pr_global r ++ 
+    spc () ++ str "must be expanded."))
 
 let print_ml_decl prm (r,_) = 
   not (to_inline r) || List.mem r prm.to_appear
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 778683646..36ccff88d 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -29,11 +29,11 @@ let rec collapse_type_app = function
   | (Tapp l1) :: l2 -> collapse_type_app (l1 @ l2)
   | l -> l
 
-let string s = [< 'sTR s >]
+let string s = (str s)
 
-let open_par = function true -> string "(" | false -> [< >]
+let open_par = function true -> string "(" | false -> (mt ())
 
-let close_par = function true -> string ")" | false -> [< >]
+let close_par = function true -> string ")" | false -> (mt ())
 
 let pp_tvar id = 
   let s = string_of_id id in 
@@ -42,32 +42,32 @@ let pp_tvar id =
   else string ("' "^s)
 
 let pp_tuple f = function
-  | [] -> [< >]
+  | [] -> (mt ())
   | [x] -> f x
-  | l -> [< 'sTR "(";
-      	    prlist_with_sep (fun () -> [< 'sTR ","; 'sPC >]) f l;
-	    'sTR ")" >]
+  | l -> (str "(" ++
+      	    prlist_with_sep (fun () -> (str "," ++ spc ())) f l ++
+	    str ")")
 
 let pp_boxed_tuple f = function
-  | [] -> [< >]
+  | [] -> (mt ())
   | [x] -> f x
-  | l -> [< 'sTR "(";
-      	    hOV 0 [< prlist_with_sep (fun () -> [< 'sTR ","; 'sPC >]) f l;
-		     'sTR ")" >] >]
+  | l -> (str "(" ++
+      	    hov 0 (prlist_with_sep (fun () -> (str "," ++ spc ())) f l ++
+		     str ")"))
 
 let pp_abst = function
-  | [] -> [< >]
-  | 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 pr_binding = function
-  | [] -> [< >]
-  | 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 -> [< >]
+let space_if = function true -> (str " ") | false -> (mt ())
 
-let sec_space_if = function true -> [< 'sPC >] | false -> [< >]
+let sec_space_if = function true -> (spc ()) | false -> (mt ())
 
 (*s Generic renaming issues. *)
 
@@ -114,10 +114,10 @@ let keywords =
   Idset.empty
 
 let preamble _ =
-  [< 'sTR "type prop = unit"; 'fNL;
-     'sTR "let prop = ()"; 'fNL; 'fNL;
-     'sTR "type arity = unit"; 'fNL;
-     'sTR "let arity = ()"; 'fNL; 'fNL >]
+  (str "type prop = unit" ++ fnl () ++
+     str "let prop = ()" ++ fnl () ++ fnl () ++
+     str "type arity = unit" ++ fnl () ++
+     str "let arity = ()" ++ fnl () ++ fnl ())
 
 (*s The pretty-printing functor. *)
 
@@ -140,12 +140,12 @@ let rec pp_type par 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::l -> (pp_tuple (pp_rec false) l ++ 
+			sec_space_if (l <>[]) ++ 
+			pp_rec false t))
     | Tarr (t1,t2) ->
-	[< open_par par; pp_rec true t1; 'sPC; 'sTR "->"; 'sPC; 
-	   pp_rec false t2; close_par par >]
+	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
+	   pp_rec false t2 ++ close_par par)
     | Tglob r -> 
 	pp_type_global r
     | Texn s -> 
@@ -155,7 +155,7 @@ let rec pp_type par t =
     | Tarity ->
 	string "arity"
   in 
-  hOV 0 (pp_rec par t)
+  hov 0 (pp_rec par t)
 
 (*s Pretty-printing of expressions. [par] indicates whether
     parentheses are needed or not. [env] is the list of names for the
@@ -171,9 +171,9 @@ let rec pp_expr par env args =
   let par' = args <> [] || par in 
   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 >] 
+    | _  -> hov 2 (open_par par ++ st ++ spc () ++
+                     prlist_with_sep (fun () -> (spc ())) (fun s -> s) args ++
+                     close_par par) 
   in
   function
     | MLrel n -> 
@@ -184,94 +184,94 @@ let rec pp_expr par env args =
     | MLlam _ as a -> 
       	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
-	[< open_par par'; st; close_par par' >]
+	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
+	(open_par par' ++ st ++ close_par par')
     | MLletin (id,a1,a2) ->
 	let id',env' = push_vars [id] env in
 	let par2 = not par' && expr_needs_par a2 in
 	apply 
-	  (hOV 0 [< open_par par';
-		    hOV 2 [< 'sTR "let "; pr_id (List.hd id'); 'sTR " ="; 'sPC;
-			     pp_expr false env [] a1; 'sPC; 'sTR "in" >];
-		    'sPC;
-		    pp_expr par2 env' [] a2;
-		    close_par par' >])
+	  (hov 0 (open_par par' ++
+		    hov 2 (str "let " ++ pr_id (List.hd id') ++ str " =" ++ spc () ++
+			     pp_expr false env [] a1 ++ spc () ++ str "in") ++
+		    spc () ++
+		    pp_expr par2 env' [] a2 ++
+		    close_par par'))
     | MLglob r -> 
 	apply (pp_global r)
     | MLcons (r,[]) ->
 	pp_global r
     | MLcons (r,[a]) ->
-	[< open_par par; pp_global r; 'sPC;
-	   pp_expr true env [] a; close_par par >]
+	(open_par par ++ pp_global r ++ spc () ++
+	   pp_expr true env [] a ++ close_par par)
     | MLcons (r,args') ->
-	[< open_par par; pp_global r; 'sPC;
-	   pp_tuple (pp_expr true env []) args'; close_par par >]
+	(open_par par ++ pp_global r ++ spc () ++
+	   pp_tuple (pp_expr true env []) args' ++ close_par par)
     | MLcase (t,[|x|])->
 	apply 
-	  (hOV 0 [< open_par par'; 'sTR "let ";  
+	  (hov 0 (open_par par' ++ str "let " ++  
 		    pp_one_pat 
-		      [< 'sTR " ="; 'sPC;
-			 pp_expr false env [] t; 'sPC; 'sTR "in" >] 
-		      env x;
-		    close_par par' >])
+		      (str " =" ++ spc () ++
+			 pp_expr false env [] t ++ spc () ++ str "in") 
+		      env x ++
+		    close_par par'))
     | MLcase (t, pv) ->
       	apply
-      	  [< open_par par';
-      	     v 0 [< 'sTR "match "; pp_expr false env [] t; 'sTR " with";
-		    'fNL; 'sTR "  "; pp_pat env pv >];
-	     close_par par' >]
+      	  (open_par par' ++
+      	     v 0 (str "match " ++ pp_expr false env [] t ++ str " with" ++
+		    fnl () ++ str "  " ++ pp_pat env pv) ++
+	     close_par par')
     | 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
-    | MLexn str -> 
-	[< open_par par; 'sTR "assert false"; 'sPC; 
-	   'sTR ("(* "^str^" *)"); close_par par >]
+    | MLexn s -> 
+	(open_par par ++ str "assert false" ++ spc () ++ 
+	   str ("(* "^s^" *)") ++ close_par par)
     | MLprop ->
 	string "prop"
     | MLarity ->
 	string "arity"
     | MLcast (a,t) ->
-	[< open_par true; pp_expr false env args a; 'sPC; 'sTR ":"; 'sPC; 
-	   pp_type false t; close_par true >]
+	(open_par true ++ pp_expr false env args a ++ spc () ++ str ":" ++ spc () ++ 
+	   pp_type false t ++ close_par true)
     | MLmagic a ->
-	[< open_par true; 'sTR "Obj.magic"; 'sPC; 
-	   pp_expr false env args a; close_par true >]
+	(open_par true ++ str "Obj.magic" ++ spc () ++ 
+	   pp_expr false env args a ++ close_par true)
 
 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 [< >] 
-     else [< 'sTR " "; pp_boxed_tuple pr_id (List.rev ids) >];
-     s; 'sPC; pp_expr par env' [] t >]
+  (pp_global r ++ 
+     if ids = [] then (mt ()) 
+     else (str " " ++ pp_boxed_tuple pr_id (List.rev ids)) ++
+     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 (string " ->") env x)) 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 [< 'sTR "let rec " ;
+  (open_par par ++ 
+     v 0 (str "let rec " ++
 	    prvect_with_sep
-      	      (fun () -> [< 'fNL; 'sTR "and " >])
+      	      (fun () -> (fnl () ++ str "and "))
 	      (fun (fi,ti) -> pp_function env (pr_id fi) ti)
-	      (array_map2 (fun id b -> (id,b)) ids bl);
-	    'fNL;
+	      (array_map2 (fun id b -> (id,b)) ids bl) ++
+	    fnl () ++
 	    match in_p with
 	      | Some j -> 
-      		  hOV 2 [< 'sTR "in "; pr_id (ids.(j));
+      		  hov 2 (str "in " ++ pr_id (ids.(j)) ++
 			   if args <> [] then
-			     [< 'sTR " "; 
-				prlist_with_sep (fun () -> [<'sTR " ">])
-				  (fun s -> s) args >]
+			     (str " " ++ 
+				prlist_with_sep (fun () -> (str " "))
+				  (fun s -> s) args)
 			   else
-			     [< >] >]
+			     (mt ()))
 	      | None -> 
-		  [< >] >];
-     close_par par >]
+		  (mt ())) ++
+     close_par par)
 
 and pp_function env f t =
   let bl,t' = collect_lams t in
@@ -283,77 +283,77 @@ and pp_function env f t =
   match t' with 
     | MLcase(MLrel 1,pv) ->
 	if is_function pv then
-	  [< f; pr_binding (List.rev (List.tl bl)) ;
-       	     'sTR " = function"; 'fNL;
-	     v 0 [< 'sTR "  "; pp_pat env' pv >] >]
+	  (f ++ pr_binding (List.rev (List.tl bl)) ++
+       	     str " = function" ++ fnl () ++
+	     v 0 (str "  " ++ pp_pat env' pv))
 	else
-          [< f; pr_binding (List.rev bl); 
-             'sTR " = match ";
-	     pr_id (List.hd bl); 'sTR " with"; 'fNL;
-	     v 0 [< 'sTR "  "; pp_pat env' pv >] >]
+          (f ++ pr_binding (List.rev bl) ++ 
+             str " = match " ++
+	     pr_id (List.hd bl) ++ str " with" ++ fnl () ++
+	     v 0 (str "  " ++ pp_pat env' pv))
 	  
-    | _ -> [< f; pr_binding (List.rev bl);
-	      'sTR " ="; 'fNL; 'sTR "  ";
-	      hOV 2 (pp_expr false env' [] t') >]
+    | _ -> (f ++ pr_binding (List.rev bl) ++
+	      str " =" ++ fnl () ++ str "  " ++
+	      hov 2 (pp_expr false env' [] t'))
 	
-let pp_ast a = hOV 0 (pp_expr false (empty_env ()) [] a)
+let pp_ast a = hov 0 (pp_expr false (empty_env ()) [] a)
 
 (*s Pretty-printing of inductive types declaration. *)
 
 let pp_parameters l = 
-  [< pp_tuple pp_tvar l; space_if (l<>[]) >]
+  (pp_tuple pp_tvar l ++ space_if (l<>[]))
 
 let pp_one_inductive (pl,name,cl) =
   let pp_constructor (id,l) =
-    [< pp_global id;
+    (pp_global id ++
        match l with
-         | [] -> [< >] 
-	 | _  -> [< 'sTR " of " ;
+         | [] -> (mt ()) 
+	 | _  -> (str " of " ++
       	       	    prlist_with_sep 
-		      (fun () -> [< 'sPC ; 'sTR "* " >]) (pp_type true) l >] >]
+		      (fun () -> (spc () ++ str "* ")) (pp_type true) l))
   in
-  [< pp_parameters pl; pp_type_global name; 'sTR " ="; 
-     [< 'fNL;
-	v 0 [< 'sTR "    ";
-	       prlist_with_sep (fun () -> [< 'fNL; 'sTR "  | " >])
-                 (fun c -> hOV 2 (pp_constructor c)) cl >] >] >]
+  (pp_parameters pl ++ pp_type_global name ++ str " =" ++ 
+     (fnl () ++
+	v 0 (str "    " ++
+	       prlist_with_sep (fun () -> (fnl () ++ str "  | "))
+                 (fun c -> hov 2 (pp_constructor c)) cl)))
   
 let pp_inductive il =
-  [< 'sTR "type ";
-     prlist_with_sep (fun () -> [< 'fNL; 'sTR "and " >]) pp_one_inductive il;
-     'fNL >]
+  (str "type " ++
+     prlist_with_sep (fun () -> (fnl () ++ str "and ")) pp_one_inductive il ++
+     fnl ())
 
 (*s Pretty-printing of a declaration. *)
 
 let warning_coinductive r = 
-  wARN (hOV 0 
-	  [< 'sTR "You are trying to extract the CoInductive definition"; 'sPC;
-	     Printer.pr_global r; 'sPC; 'sTR "in Ocaml."; 'sPC; 
-	     'sTR "This is in general NOT a good idea,"; 'sPC; 
-	     'sTR "since Ocaml is not lazy."; 'sPC;
-	     'sTR "You should consider using Haskell instead." >])
+  warn (hov 0 
+	  (str "You are trying to extract the CoInductive definition" ++ spc () ++
+	     Printer.pr_global r ++ spc () ++ str "in Ocaml." ++ spc () ++ 
+	     str "This is in general NOT a good idea," ++ spc () ++ 
+	     str "since Ocaml is not lazy." ++ spc () ++
+	     str "You should consider using Haskell instead."))
 
 let pp_decl = function
   | Dtype ([], _) -> 
-      if P.toplevel then hOV 0 [< 'sTR " prop (* Logic inductive *)"; 'fNL >]
-      else [< >] 
+      if P.toplevel then hov 0 (str " prop (* Logic inductive *)" ++ fnl ())
+      else (mt ()) 
   | Dtype ((_,r,_)::_ as i, cofix) -> 
       if cofix && (not P.toplevel) then if_verbose warning_coinductive r; 
-      hOV 0 (pp_inductive i)
+      hov 0 (pp_inductive i)
   | Dabbrev (r, l, t) ->
-      hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; 
-	       pp_type_global r; 'sPC; 'sTR "="; 'sPC; 
-	       pp_type false  t; 'fNL >]
+      hov 0 (str "type" ++ spc () ++ pp_parameters l ++ 
+	       pp_type_global r ++ spc () ++ str "=" ++ spc () ++ 
+	       pp_type false  t ++ fnl ())
   | Dglob (r, MLfix (_,[|_|],[|def|])) ->
       let id = rename_global r in
       let env' = [id], P.globals() in
-      [<  hOV 2 (pp_fix false env' None ([|id|],[|def|]) []) >]
+      (hov 2 (pp_fix false env' None ([|id|],[|def|]) []))
   | Dglob (r, a) ->
-      hOV 0 [< 'sTR "let "; 
-	       pp_function (empty_env ()) (pp_global r) a; 'fNL >]
+      hov 0 (str "let " ++ 
+	       pp_function (empty_env ()) (pp_global r) a ++ fnl ())
   | Dcustom (r,s) -> 
-      hOV 0 [< 'sTR "let "; pp_global r; 
-	       'sTR " ="; 'sPC; 'sTR s; 'fNL >]
+      hov 0 (str "let " ++ pp_global r ++ 
+	       str " =" ++ spc () ++ str s ++ fnl ())
 
 let pp_type = pp_type false
 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 8c8138fd0..a45490f20 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -64,7 +64,7 @@ let is_constant r = match r with
 let check_constant r = 
   if (is_constant r) then r 
   else errorlabstrm "extract_constant"
-	[< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >] 
+	(Printer.pr_global r ++ spc () ++ str "is not a constant") 
 
 let string_of_varg = function
   | VARG_IDENTIFIER id -> string_of_id id
@@ -73,7 +73,7 @@ let string_of_varg = function
 
 let no_such_reference q =
   errorlabstrm "reference_of_varg" 
-    [< Nametab.pr_qualid q; 'sTR ": no such reference" >]
+    (Nametab.pr_qualid q ++ str ": no such reference")
 
 let reference_of_varg = function
   | VARG_QUALID q -> 
@@ -135,14 +135,14 @@ let _ =
 let print_inline () = 
   let (i,n)= !inline_table in 
   let i'= Refset.filter is_constant i in 
-  mSG 
-    [< 'sTR "Extraction Inline:"; 'fNL; 
+  msg 
+    (str "Extraction Inline:" ++ fnl () ++ 
        Refset.fold
-	 (fun r p -> [< p; 'sTR "   " ; Printer.pr_global r ; 'fNL >]) i' [<>];
-       'sTR "Extraction NoInline:"; 'fNL; 
+	 (fun r p -> (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++
+       str "Extraction NoInline:" ++ fnl () ++ 
        Refset.fold
-	 (fun r p -> [< p; 'sTR "   " ; Printer.pr_global r ; 'fNL >]) n [<>]
-    >]
+	 (fun r p -> (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) n (mt ())
+)
 
 let _ = vinterp_add "PrintExtractionInline" (fun _ -> print_inline)
 
@@ -237,7 +237,7 @@ let extract_inductive r (id2,l2) = match r with
 	   add_anonymous_leaf (in_ml_extraction (r,s))) l2
   | _ -> 
       errorlabstrm "extract_inductive"
-	[< Printer.pr_global r; 'sPC; 'sTR "is not an inductive type" >]
+	(Printer.pr_global r ++ spc () ++ str "is not an inductive type")
 
 let _ = 
   vinterp_add "ExtractInductive"