compat ocaml 3.03

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

29 files changed, 658 insertions, 650 deletions

diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml
index 4663b3e370..63c1762175 100644
--- a/contrib/correctness/pcicenv.ml
+++ b/contrib/correctness/pcicenv.ml
@@ -27,7 +27,7 @@ let modify_sign id t s =
   fold_named_context
     (fun ((x,b,ty) as d) sign ->
       if x=id then add_named_decl (x,b,t) sign else add_named_decl d sign)
-    s empty_named_context
+    s ~init:empty_named_context
 
 let add_sign (id,t) s =
   try 
diff --git a/contrib/correctness/peffect.ml b/contrib/correctness/peffect.ml
index 1db31269b9..c6e1636c62 100644
--- a/contrib/correctness/peffect.ml
+++ b/contrib/correctness/peffect.ml
@@ -143,17 +143,17 @@ open Util
 open Himsg
 
 let pp (r,w) =
-  hOV 0 [< if r<>[] then
-	     [< 'sTR"reads ";
-		prlist_with_sep (fun () -> [< 'sTR","; 'sPC >]) pr_id r >]
-	   else [< >];
-	   'sPC;
+  hov 0 (if r<>[] then
+	     (str"reads " ++
+		prlist_with_sep (fun () -> (str"," ++ spc ())) pr_id r)
+	   else (mt ()) ++
+	   spc () ++
 	   if w<>[] then
-	     [< 'sTR"writes ";
-		prlist_with_sep (fun ()-> [< 'sTR","; 'sPC >]) pr_id w >]
-	   else [< >]
-	>]
+	     (str"writes " ++
+		prlist_with_sep (fun ()-> (str"," ++ spc ())) pr_id w)
+	   else (mt ())
+)
 
 let ppr e =
-  pP (pp e)
+  Pp.pp (pp e)
 
diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index c3cc1ec64a..9ac7bee8e3 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -223,7 +223,7 @@ let register id id' =
     let (v,p) = Idmap.find id !edited in
     let _ = add_global id' v (Some p) in
     Options.if_verbose 
-      mSGNL (hOV 0 [< 'sTR"Program "; pr_id id'; 'sPC; 'sTR"is defined" >]);
+      msgnl (hov 0 (str"Program " ++ pr_id id' ++ spc () ++ str"is defined"));
     edited := Idmap.remove id !edited
   with Not_found -> ()
 
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 17c673a543..19b4db9928 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -30,38 +30,38 @@ let raise_with_loc = function
 let unbound_variable id loc =
   raise_with_loc loc
     (UserError ("Perror.unbound_variable",
-    (hOV 0 [<'sTR"Unbound variable"; 'sPC; pr_id id; 'fNL >])))
+    (hov 0 (str"Unbound variable" ++ spc () ++ pr_id id ++ fnl ()))))
 
 let unbound_reference id loc =
   raise_with_loc loc
     (UserError ("Perror.unbound_reference",
-    (hOV 0 [<'sTR"Unbound reference"; 'sPC; pr_id id; 'fNL >])))
+    (hov 0 (str"Unbound reference" ++ spc () ++ pr_id id ++ fnl ()))))
 
 let clash id loc =
   raise_with_loc loc
     (UserError ("Perror.clash",
-    (hOV 0 [< 'sTR"Clash with previous constant"; 'sPC;
-    'sTR(string_of_id id); 'fNL >])))
+    (hov 0 (str"Clash with previous constant" ++ spc () ++
+    str(string_of_id id) ++ fnl ()))))
 
 let not_defined id =
   raise
     (UserError ("Perror.not_defined",
-	       	(hOV 0 [< 'sTR"The object"; 'sPC; pr_id id; 'sPC;
-			  'sTR"is not defined"; 'fNL >])))
+	       	(hov 0 (str"The object" ++ spc () ++ pr_id id ++ spc () ++
+			  str"is not defined" ++ fnl ()))))
 
 let check_for_reference loc id = function
     Ref _ -> ()
   | _ -> Stdpp.raise_with_loc loc 
 	(UserError ("Perror.check_for_reference",
-		    hOV 0 [< pr_id id; 'sPC; 
-			     'sTR"is not a reference" >]))
+		    hov 0 (pr_id id ++ spc () ++ 
+			     str"is not a reference")))
 
 let check_for_array loc id = function
     Array _ -> ()
   | _ -> Stdpp.raise_with_loc loc 
 	(UserError ("Perror.check_for_array",
-		    hOV 0 [< pr_id id; 'sPC; 
-			     'sTR"is not an array" >]))
+		    hov 0 (pr_id id ++ spc () ++ 
+			     str"is not an array")))
 
 let is_constant_type s = function
     TypePure c ->
@@ -75,56 +75,56 @@ let check_for_index_type loc v =
   if not is_index then
     Stdpp.raise_with_loc loc 
       (UserError ("Perror.check_for_index",
-		  hOV 0 [< 'sTR"This expression is an index"; 'sPC; 
-			   'sTR"and should have type int (Z)" >]))
+		  hov 0 (str"This expression is an index" ++ spc () ++ 
+			   str"and should have type int (Z)")))
 
 let check_no_effect loc ef =
   if not (Peffect.get_writes ef = []) then
     Stdpp.raise_with_loc loc 
       (UserError ("Perror.check_no_effect",
-		  hOV 0 [< 'sTR"A boolean should not have side effects"
-		        >]))
+		  hov 0 (str"A boolean should not have side effects"
+)))
 
 let should_be_boolean loc =
   Stdpp.raise_with_loc loc 
     (UserError ("Perror.should_be_boolean",
-		hOV 0 [< 'sTR"This expression is a test:" ; 'sPC;
-			 'sTR"it should have type bool" >]))
+		hov 0 (str"This expression is a test:" ++ spc () ++
+			 str"it should have type bool")))
 
 let test_should_be_annotated loc =
   Stdpp.raise_with_loc loc 
     (UserError ("Perror.test_should_be_annotated",
-		hOV 0 [< 'sTR"This test should be annotated" >]))
+		hov 0 (str"This test should be annotated")))
 
 let if_branches loc =
   Stdpp.raise_with_loc loc 
     (UserError ("Perror.if_branches",
-		hOV 0 [< 'sTR"The two branches of an `if' expression" ; 'sPC;
-			 'sTR"should have the same type" >]))
+		hov 0 (str"The two branches of an `if' expression" ++ spc () ++
+			 str"should have the same type")))
 
 let check_for_not_mutable loc v =
   if is_mutable v then
     Stdpp.raise_with_loc loc 
       (UserError ("Perror.check_for_not_mutable",
-		  hOV 0 [< 'sTR"This expression cannot be a mutable" >]))
+		  hov 0 (str"This expression cannot be a mutable")))
 
 let check_for_pure_type loc v =
   if not (is_pure v) then
     Stdpp.raise_with_loc loc 
       (UserError ("Perror.check_for_pure_type",
-		  hOV 0 [< 'sTR"This expression must be pure"; 'sPC;
-			   'sTR"(neither a mutable nor a function)" >]))
+		  hov 0 (str"This expression must be pure" ++ spc () ++
+			   str"(neither a mutable nor a function)")))
 
 let check_for_let_ref loc v =
   if not (is_pure v) then
     Stdpp.raise_with_loc loc 
       (UserError ("Perror.check_for_let_ref",
-		  hOV 0 [< 'sTR"References can only be bound in pure terms">]))
+		  hov 0 (str"References can only be bound in pure terms")))
 
 let informative loc s =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.variant_informative",
-	      hOV 0 [< 'sTR s; 'sPC; 'sTR"must be informative" >]))
+	      hov 0 (str s ++ spc () ++ str"must be informative")))
 
 let variant_informative loc = informative loc "Variant"
 let should_be_informative loc = informative loc "This term"
@@ -132,41 +132,41 @@ let should_be_informative loc = informative loc "This term"
 let app_of_non_function loc =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.app_of_non_function",
-	      hOV 0 [< 'sTR"This term cannot be applied"; 'sPC;
-		       'sTR"(either it is not a function"; 'sPC;
-		       'sTR"or it is applied to non pure arguments)" >]))
+	      hov 0 (str"This term cannot be applied" ++ spc () ++
+		       str"(either it is not a function" ++ spc () ++
+		       str"or it is applied to non pure arguments)")))
   
 let partial_app loc =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.partial_app",
-	      hOV 0 [< 'sTR"This function does not have";
-		       'sPC; 'sTR"the right number of arguments" >]))
+	      hov 0 (str"This function does not have" ++
+		       spc () ++ str"the right number of arguments")))
   
 let expected_type loc s =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.expected_type",
-	      hOV 0 [< 'sTR"Argument is expected to have type"; 'sPC; s >]))
+	      hov 0 (str"Argument is expected to have type" ++ spc () ++ s)))
 
 let expects_a_type id loc =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.expects_a_type",
-	      hOV 0 [< 'sTR"The argument "; pr_id id; 'sPC;
-		       'sTR"in this application is supposed to be a type" >]))
+	      hov 0 (str"The argument " ++ pr_id id ++ spc () ++
+		       str"in this application is supposed to be a type")))
 
 let expects_a_term id =
   raise
   (UserError ("Perror.expects_a_type",
-	      hOV 0 [< 'sTR"The argument "; pr_id id; 'sPC;
-		       'sTR"in this application is supposed to be a term" >]))
+	      hov 0 (str"The argument " ++ pr_id id ++ spc () ++
+		       str"in this application is supposed to be a term")))
 
 let should_be_a_variable loc =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.should_be_a_variable",
-	      hOV 0 [< 'sTR"Argument should be a variable" >]))
+	      hov 0 (str"Argument should be a variable")))
    
 let should_be_a_reference loc =
   Stdpp.raise_with_loc loc 
   (UserError ("Perror.should_be_a_reference",
-	      hOV 0 [< 'sTR"Argument of function should be a reference" >]))
+	      hov 0 (str"Argument of function should be a reference")))
 
    
diff --git a/contrib/correctness/pextract.ml b/contrib/correctness/pextract.ml
index a097ac1b59..47fc9929f7 100644
--- a/contrib/correctness/pextract.ml
+++ b/contrib/correctness/pextract.ml
@@ -42,18 +42,18 @@ let access = ConstRef sp_access
 let has_array = ref false
 
 let pp_conversions () =
-  [< 'sTR"\
+  (str"\
 let rec int_of_pos = function
     XH -> 1
   | XI p -> 2 * (int_of_pos p) + 1
   | XO p -> 2 * (int_of_pos p)
-;;
+ ++ ++
 
 let int_of_z = function
     ZERO -> 0
   | POS p -> int_of_pos p
   | NEG p -> -(int_of_pos p)
-;;
+ ++ ++
 " >] (* '"' *)
 
 (* collect all section-path in a CIC constant *)
@@ -61,7 +61,7 @@ let int_of_z = function
 let spset_of_cci env c =
   let spl = Fw_env.collect (extraction env c) in
   let sps = List.fold_left (fun e x -> SpSet.add x e) SpSet.empty spl in
-  has_array := !has_array or (SpSet.mem sp_access sps);
+  has_array := !has_array or (SpSet.mem sp_access sps) ++
   SpSet.remove sp_access sps
 
 
@@ -81,10 +81,10 @@ let collect env =
     | Acc x -> add_id env s x
     | Aff (x,e1) -> add_id env (collect_rec env s e1) x
     | TabAcc (_,x,e1) ->
-	has_array := true;
+	has_array := true ++
 	add_id env (collect_rec env s e1) x
     | TabAff (_,x,e1,e2) ->
-	has_array := true;
+	has_array := true ++
 	add_id env (collect_rec env (collect_rec env s e1) e2) x
     | Seq bl ->
 	List.fold_left (fun s st -> match st with
@@ -144,17 +144,17 @@ module Ocaml_ren = Ocaml.OCaml_renaming
 
 let rename_global id =
   let id' = Ocaml_ren.rename_global_term !Fwtoml.globals (Name id) in
-  Fwtoml.add_global_renaming (id,id');
+  Fwtoml.add_global_renaming (id,id') ++
   id'
 
-type rename_struct = { rn_map : identifier IdMap.t;
+type rename_struct = { rn_map : identifier IdMap.t ++
 		       rn_avoid : identifier list }
 
-let rn_empty = { rn_map = IdMap.empty; rn_avoid = [] }
+let rn_empty = { rn_map = IdMap.empty ++ rn_avoid = [] }
 
 let rename_local rn id =
   let id' = Ocaml_ren.rename_term (!Fwtoml.globals@rn.rn_avoid) (Name id) in
-  { rn_map = IdMap.add id id' rn.rn_map; rn_avoid = id' :: rn.rn_avoid },
+  { rn_map = IdMap.add id id' rn.rn_map ++ rn_avoid = id' :: rn.rn_avoid },
   id'
 
 let get_local_name rn id = IdMap.find id rn.rn_map
@@ -177,7 +177,7 @@ let rec rename_binders rn = function
  *)
 
 let putpar par s =
-  if par then [< 'sTR"("; s; 'sTR")" >] else s
+  if par then (str"(" ++ s ++ str")") else s
 
 let is_ref env id =
   try
@@ -188,21 +188,21 @@ let is_ref env id =
 let rec pp_constr env rn = function
   | VAR id ->
       if is_ref env id then 
-	[< 'sTR"!"; pID (get_name env rn id) >] 
+	(str"!" ++ pID (get_name env rn id)) 
       else
 	pID (get_name env rn id)
   | DOPN((Const _|MutInd _|MutConstruct _) as oper, _) ->
       pID (Fwtoml.name_of_oper oper)
   | DOPN(AppL,v) ->
       if Array.length v = 0 then
-	  [< >]
+	  (mt ())
       else begin
 	match v.(0) with
 	    DOPN(Const sp,_) when sp = sp_access ->
-	      [< pp_constr env rn v.(3); 
-		 'sTR".(int_of_z "; pp_constr env rn v.(4); 'sTR")" >]
+	      (pp_constr env rn v.(3) ++ 
+		 str".(int_of_z " ++ pp_constr env rn v.(4) ++ str")")
 	  | _ ->
-	      hOV 2 (putpar true (prvect_with_sep (fun () -> [< 'sPC >])
+	      hov 2 (putpar true (prvect_with_sep (fun () -> (spc ()))
 				    (pp_constr env rn) v))
       end
   | DOP2(Cast,c,_) -> pp_constr env rn c
@@ -219,95 +219,95 @@ let collect_lambda =
   collect []
 
 let pr_binding rn = 
-  prlist_with_sep (fun () -> [< >])
+  prlist_with_sep (fun () -> (mt ()))
     (function 
        | (id,(Untyped | BindType _)) -> 
-	   [< 'sTR" "; pID (get_local_name rn id) >]
-       | (id,BindSet) -> [< >])
+	   (str" " ++ pID (get_local_name rn id))
+       | (id,BindSet) -> (mt ()))
 
 let pp_prog id =
   let rec pp_d env rn par = function
     | Var x -> pID (get_name env rn x)
-    | Acc x -> [< 'sTR"!"; pID (get_name env rn x) >]
-    | Aff (x,e1) -> [< pID (get_name env rn x); 
-		       'sTR" := "; hOV 0 (pp env rn false e1) >]
+    | Acc x -> (str"!" ++ pID (get_name env rn x))
+    | Aff (x,e1) -> (pID (get_name env rn x) ++ 
+		       str" := " ++ hov 0 (pp env rn false e1))
     | TabAcc (_,x,e1) ->
-	[< pID (get_name env rn x); 
-	   'sTR".(int_of_z "; hOV 0 (pp env rn true e1); 'sTR")" >]
+	(pID (get_name env rn x) ++ 
+	   str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")")
     | TabAff (_,x,e1,e2) ->
-	[< pID (get_name env rn x);
-	   'sTR".(int_of_z "; hOV 0 (pp env rn true e1); 'sTR")";
-	   'sTR" <-"; 'sPC; hOV 2 (pp env rn false e2) >]
+	(pID (get_name env rn x) ++
+	   str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")" ++
+	   str" <-" ++ spc () ++ hov 2 (pp env rn false e2))
     | Seq bl ->
-	[< 'sTR"begin"; 'fNL;
-	   'sTR"  "; hOV 0 [< pp_block env rn bl; >]; 'fNL;
-	   'sTR"end" >]
+	(str"begin" ++ fnl () ++
+	   str"  " ++ hov 0 (pp_block env rn bl ++) ++ fnl () ++
+	   str"end")
     | If (e1,e2,e3) ->
-	putpar par [< 'sTR"if "; (pp env rn false e1);
-		      'sTR" then"; 'fNL;
-		      'sTR"  "; hOV 0 (pp env rn false e2); 'fNL;
-		      'sTR"else"; 'fNL;
-		      'sTR"  "; hOV 0 (pp env rn false e3) >]
+	putpar par (str"if " ++ (pp env rn false e1) ++
+		      str" then" ++ fnl () ++
+		      str"  " ++ hov 0 (pp env rn false e2) ++ fnl () ++
+		      str"else" ++ fnl () ++
+		      str"  " ++ hov 0 (pp env rn false e3))
 	(* optimisations : then begin .... end else begin ... end *)
     | While (b,inv,_,bl) ->
-	[< 'sTR"while "; (pp env rn false b); 'sTR" do"; 'fNL;		    
-	   'sTR"  ";
-	   hOV 0 [< (match inv with
-			 None -> [< >] 
-		       | Some c -> [< 'sTR"(* invariant: "; pTERM c.a_value ; 
-				      'sTR" *)"; 'fNL >]);
-		    pp_block env rn bl; >]; 'fNL;
-	   'sTR"done"; >]
+	(str"while " ++ (pp env rn false b) ++ str" do" ++ fnl () ++		    
+	   str"  " ++
+	   hov 0 ((match inv with
+			 None -> (mt ()) 
+		       | Some c -> (str"(* invariant: " ++ pTERM c.a_value ++ 
+				      str" *)" ++ fnl ())) ++
+		    pp_block env rn bl ++) ++ fnl () ++
+	   str"done" ++)
     | Lam (bl,e) ->
 	let env' = traverse_binders env bl in
 	let rn' = rename_binders rn bl in
 	  putpar par 
-	    (hOV 2 [< 'sTR"fun"; pr_binding rn' bl; 'sTR" ->";
-		      'sPC; pp env' rn' false e >])
-    | SApp ((Var id)::_,  [e1; e2])
+	    (hov 2 (str"fun" ++ pr_binding rn' bl ++ str" ->" ++
+		      spc () ++ pp env' rn' false e))
+    | SApp ((Var id)::_,  [e1 ++ e2])
 	when id = connective_and or id = connective_or ->
 	  let conn = if id = connective_and then "&" else "or" in
 	  putpar par 
-	    (hOV 0 [< pp env rn true e1; 'sPC; 'sTR conn; 'sPC;
-		      pp env rn true e2 >])
+	    (hov 0 (pp env rn true e1 ++ spc () ++ str conn ++ spc () ++
+		      pp env rn true e2))
     | SApp ((Var id)::_, [e]) when id = connective_not ->
 	putpar par 
-	  (hOV 0 [< 'sTR"not"; 'sPC; pp env rn true e >])
+	  (hov 0 (str"not" ++ spc () ++ pp env rn true e))
     | SApp _ ->
 	invalid_arg "Prog_extract.pp_prog (SApp)"
     | App(e1,[]) ->
-	hOV 0 (pp env rn false e1)
+	hov 0 (pp env rn false e1)
     | App (e1,l) ->
 	putpar true
-	  (hOV 2 [< pp env rn true e1;
+	  (hov 2 (pp env rn true e1 ++
 		    prlist (function 
-				Term p -> [< 'sPC; pp env rn true p >]
-			      | Refarg x -> [< 'sPC; pID (get_name env rn x) >]
-			      | Type _ -> [< >]) 
-		      l >])
+				Term p -> (spc () ++ pp env rn true p)
+			      | Refarg x -> (spc () ++ pID (get_name env rn x))
+			      | Type _ -> (mt ())) 
+		      l))
     | LetRef (x,e1,e2) ->
 	let (_,v),_,_,_ = e1.info.kappa in
 	let env' = add (x,Ref v) env in
 	let rn',x' = rename_local rn x in
 	putpar par 
-	  (hOV 0 [< 'sTR"let "; pID x'; 'sTR" = ref "; pp env rn false e1;
-		    'sTR" in"; 'fNL; pp env' rn' false e2 >])
+	  (hov 0 (str"let " ++ pID x' ++ str" = ref " ++ pp env rn false e1 ++
+		    str" in" ++ fnl () ++ pp env' rn' false e2))
     | LetIn (x,e1,e2) ->
 	let (_,v),_,_,_ = e1.info.kappa in
 	let env' = add (x,v) env in
 	let rn',x' = rename_local rn x in
 	putpar par 
-	  (hOV 0 [< 'sTR"let "; pID x'; 'sTR" = "; pp env rn false e1;
-		    'sTR" in"; 'fNL; pp env' rn' false e2 >])
+	  (hov 0 (str"let " ++ pID x' ++ str" = " ++ pp env rn false e1 ++
+		    str" in" ++ fnl () ++ pp env' rn' false e2))
     | LetRec (f,bl,_,_,e) ->
 	let env' = traverse_binders env bl in
 	let rn' = rename_binders rn bl in
 	let env'' = add (f,make_arrow bl e.info.kappa) env' in
 	let rn'',f' = rename_local rn' f in
 	putpar par 
-	  (hOV 0 [< 'sTR"let rec "; pID f'; pr_binding rn' bl; 'sTR" ="; 'fNL;
-		    'sTR"  "; hOV 0 [< pp env'' rn'' false e >]; 'fNL;
-		    'sTR"in "; pID f' >])
+	  (hov 0 (str"let rec " ++ pID f' ++ pr_binding rn' bl ++ str" =" ++ fnl () ++
+		    str"  " ++ hov 0 (pp env'' rn'' false e) ++ fnl () ++
+		    str"in " ++ pID f'))
     | Debug (_,e1) -> pp env rn par e1
     | PPoint (_,d) -> pp_d env rn par d
     | Expression c -> 
@@ -317,21 +317,21 @@ let pp_prog id =
     let bl =
       map_succeed (function Statement p -> p | _ -> failwith "caught") bl
     in
-      prlist_with_sep (fun () -> [< 'sTR";"; 'fNL >])
-      	(fun p -> hOV 0 (pp env rn false p)) bl
+      prlist_with_sep (fun () -> (str";" ++ fnl ()))
+      	(fun p -> hov 0 (pp env rn false p)) bl
 
   and pp env rn par p = 
-    [< pp_d env rn par p.desc >]
+    (pp_d env rn par p.desc)
 
   and pp_mut v c = match v with
     | Ref _ ->
-	[< 'sTR"ref "; pp_constr empty rn_empty (extraction empty c) >]
+	(str"ref " ++ pp_constr empty rn_empty (extraction empty c))
     | Array (n,_) ->
-	[< 'sTR"Array.create "; 'cUT;
+	(str"Array.create " ++ cut () ++
 	   putpar true 
-	     [< 'sTR"int_of_z ";
-		pp_constr empty rn_empty (extraction empty n) >];
-	   'sTR" "; pp_constr empty rn_empty (extraction empty c) >]
+	     (str"int_of_z " ++
+		pp_constr empty rn_empty (extraction empty n)) ++
+	   str" " ++ pp_constr empty rn_empty (extraction empty c))
     | _ -> invalid_arg "pp_mut"
   in
   let v = lookup_global id in
@@ -339,23 +339,23 @@ let pp_prog id =
     if is_mutable v then
       try
 	let c = find_init id in
-	hOV 0 [< 'sTR"let "; pID id'; 'sTR" = "; pp_mut v c >]
+	hov 0 (str"let " ++ pID id' ++ str" = " ++ pp_mut v c)
       with Not_found -> 
 	errorlabstrm "Prog_extract.pp_prog"
-	  [< 'sTR"The variable "; pID id;
-	     'sTR" must be initialized first !" >]
+	  (str"The variable " ++ pID id ++
+	     str" must be initialized first !")
     else
       match find_pgm id with
 	| None -> 
 	    errorlabstrm "Prog_extract.pp_prog"
-	      [< 'sTR"The program "; pID id;
-		 'sTR" must be realized first !" >]
+	      (str"The program " ++ pID id ++
+		 str" must be realized first !")
       	| Some p ->
 	    let bl,p = collect_lambda p in
 	    let rn = rename_binders rn_empty bl in
 	    let env = traverse_binders empty bl in
-	    hOV 0  [< 'sTR"let "; pID id'; pr_binding rn bl; 'sTR" ="; 'fNL; 
-		      'sTR"  "; hOV 2 (pp env rn false p) >]
+	    hov 0  (str"let " ++ pID id' ++ pr_binding rn bl ++ str" =" ++ fnl () ++ 
+		      str"  " ++ hov 2 (pp env rn false p))
 
 (* extraction des programmes impératifs/fonctionnels vers ocaml *)
 
@@ -375,7 +375,7 @@ let import sp = match repr_path sp with
   | _ -> ()
 
 let pp_ocaml file prm =
-  has_array := false;
+  has_array := false ++
   (* on separe objects Coq et programmes *)
   let cic,pgms =
     List.fold_left
@@ -404,7 +404,7 @@ let pp_ocaml file prm =
 	   in
 	   let cic' = 
 	     SpSet.fold 
-	       (fun sp cic -> import sp; IdSet.add (basename sp) cic)
+	       (fun sp cic -> import sp ++ IdSet.add (basename sp) cic)
 	       spl cic
 	   in
 	   (cic',IdSet.union pgms pgms',id::pl)
@@ -414,23 +414,23 @@ let pp_ocaml file prm =
   in
   let cic = IdSet.elements cic in
   (* on pretty-print *)
-  let prm' = { needed = cic; expand = prm.expand; 
-	       expansion = prm.expansion; exact = prm.exact } 
+  let prm' = { needed = cic ++ expand = prm.expand ++ 
+	       expansion = prm.expansion ++ exact = prm.exact } 
   in
-  let strm = [< Ocaml.OCaml_pp_file.pp_recursive prm';
-		'fNL; 'fNL;
-		if !has_array then pp_conversions() else [< >];
-		prlist (fun p -> [< pp_prog p; 'fNL; 'sTR";;"; 'fNL; 'fNL >])
+  let strm = (Ocaml.OCaml_pp_file.pp_recursive prm' ++
+		fnl () ++ fnl () ++
+		if !has_array then pp_conversions() else (mt ()) ++
+		prlist (fun p -> (pp_prog p ++ fnl () ++ str";;" ++ fnl () ++ fnl ()))
 		  pgms
-	     >]
+)
   in
   (* puis on ecrit dans le fichier *)
   let chan = open_trapping_failure open_out file ".ml" in
   let ft = with_output_to chan in
   begin
-    try  pP_with ft strm ; pp_flush_with ft ()
-    with e -> pp_flush_with ft () ; close_out chan; raise e
-  end;
+    try  pP_with ft strm ++ pp_flush_with ft ()
+    with e -> pp_flush_with ft () ++ close_out chan ++ raise e
+  end ++
   close_out chan
     
 
@@ -450,10 +450,10 @@ let initialize id com =
       initialize id c
     else
       errorlabstrm "Prog_extract.initialize"
-	[< 'sTR"Not the expected type for the mutable "; pID id >]
+	(str"Not the expected type for the mutable " ++ pID id)
   with Not_found -> 
     errorlabstrm "Prog_extract.initialize"
-      [< pr_id id; 'sTR" is not a mutable" >]
+      (pr_id id ++ str" is not a mutable")
 
 (* grammaire *)
 
@@ -467,6 +467,6 @@ let _ = vinterp_add "IMPERATIVEEXTRACTION"
 	  
 let _ = vinterp_add "INITIALIZE"
 	  (function 
-	     | [VARG_IDENTIFIER id ; VARG_COMMAND com] ->
+	     | [VARG_IDENTIFIER id ++ VARG_COMMAND com] ->
 		 (fun () -> initialize id com)
 	     | _ -> assert false)
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 6d04befe23..36e4f0dc91 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -22,7 +22,7 @@ let debug = ref false
 
 let deb_mess s =
   if !debug then begin
-    mSGNL s;  pp_flush()
+    msgnl s;  pp_flush()
   end
 
 let list_of_some = function
diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml
index 122ff16ab5..aa068f19ce 100644
--- a/contrib/correctness/prename.ml
+++ b/contrib/correctness/prename.ml
@@ -111,8 +111,8 @@ let var_at_date r d id =
     find (until d r) id
   with Not_found ->
     raise (UserError ("Renamings.var_at_date",
-	      hOV 0 [< 'sTR"Variable "; pr_id id; 'sTR" is unknown"; 'sPC;
-		       'sTR"at date "; 'sTR d >]))
+	      hov 0 (str"Variable " ++ pr_id id ++ str" is unknown" ++ spc () ++
+		       str"at date " ++ str d)))
 
 let vars_at_date r d ids =
   let r' = until d r in List.map (fun id -> id,find r' id) ids
@@ -125,15 +125,15 @@ open Util
 open Himsg
 
 let pp r = 
-  hOV 2 (prlist_with_sep (fun () -> [< 'fNL >])
+  hov 2 (prlist_with_sep (fun () -> (fnl ()))
 	   (fun (d,l) -> 
-	      [< 'sTR d; 'sTR": "; 
-		 prlist_with_sep (fun () -> [< 'sPC >])
+	      (str d ++ str": " ++ 
+		 prlist_with_sep (fun () -> (spc ()))
 		   (fun (id,id') -> 
-		      [< 'sTR"("; pr_id id; 'sTR","; pr_id id'; 'sTR")" >])
-		   l >])
+		      (str"(" ++ pr_id id ++ str"," ++ pr_id id' ++ str")"))
+		   l))
 	   r.levels)
 
 let ppr e =
-  pP (pp e)
+  Pp.pp (pp e)
 
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 6b487348a8..3617914148 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -490,12 +490,12 @@ open Declare
 
 let is_assumed global ids =
   if List.length ids = 1 then
-    mSGNL [< 'sTR (if global then "A global variable " else ""); 
-	     pr_id (List.hd ids); 'sTR " is assumed" >]
+    msgnl (str (if global then "A global variable " else "") ++ 
+	     pr_id (List.hd ids) ++ str " is assumed")
   else
-    mSGNL [< 'sTR (if global then "Some global variables " else "");
-	     prlist_with_sep (fun () -> [< 'sTR ", " >]) pr_id ids;
-	     'sTR " are assumed" >]
+    msgnl (str (if global then "Some global variables " else "") ++
+	     prlist_with_sep (fun () -> (str ", ")) pr_id ids ++
+	     str " are assumed")
 
 let add = vinterp_add
 
@@ -521,10 +521,10 @@ let _ =
 	   (fun () ->
 	      fold_all 
 		(fun (id,v) _ -> 
-		   mSGNL [< pr_id id; 'sTR " : "; 
-			    hOV 2 (match v with TypeV v -> pp_type_v v
-				     | Set -> [< 'sTR "Set" >]);
-			    'fNL >])
+		   msgnl (pr_id id ++ str " : " ++ 
+			    hov 2 (match v with TypeV v -> pp_type_v v
+				     | Set -> (str "Set")) ++
+			    fnl ()))
 		Penv.empty ())
        | _ -> assert false)
 
@@ -539,7 +539,7 @@ let _ =
 	      List.iter
 		(fun id -> if Penv.is_global id then
 		   Util.errorlabstrm "PROGVARIABLE"
-		     [< 'sTR"Clash with previous constant "; pr_id id >])
+		     (str"Clash with previous constant " ++ pr_id id))
 		ids;
 	      let v = out_typev d in
 	      Pdb.check_type_v (all_refs ()) v;
@@ -575,13 +575,13 @@ GEXTEND Gram
 
     | IDENT "Correctness"; s = IDENT; p = Programs.program; "." ->
 	let d = Ast.dynamic (in_prog p) in
-	let str = Ast.str s in
+	let str = Ast.string s in
 	<:ast< (CORRECTNESS $str (VERNACDYN $d)) >>
 
     | IDENT "Correctness"; s = IDENT; p = Programs.program; ";";
       tac = Tactic.tactic; "." ->
 	let d = Ast.dynamic (in_prog p) in
-	let str = Ast.str s in
+	let str = Ast.string s in
 	<:ast< (CORRECTNESS $str (VERNACDYN $d) (TACTIC $tac)) >> ] ];
   Pcoq.Vernac_.command:
   [ [ IDENT "Debug"; IDENT "on"; "." -> <:ast< (PROGDEBUGON) >>
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 011c3c7e88..e8f10fc899 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -37,7 +37,7 @@ let coqast_of_prog p =
   let p = Pdb.db_prog p in
 
   (* 2. typage avec effets *)
-  deb_mess [< 'sTR"Ptyping.states: Typing with effects..."; 'fNL >];
+  deb_mess (str"Ptyping.states: Typing with effects..." ++ fnl ());
   let env = Penv.empty in
   let ren = initial_renaming env in
   let p = Ptyping.states ren env p in
@@ -54,20 +54,20 @@ let coqast_of_prog p =
 
   (* 4b. traduction terme (terme intermédiaire de type cc_term) *)
   deb_mess 
-    [< 'fNL; 'sTR"Mlize.trad: Translation program -> cc_term..."; 'fNL >];
+    (fnl () ++ str"Mlize.trad: Translation program -> cc_term..." ++ fnl ());
   let cc = Pmlize.trans ren p in
   let cc = Pred.red cc in
   deb_mess (Putil.pp_cc_term cc);
 
   (* 5. traduction en constr *)
   deb_mess 
-    [< 'fNL; 'sTR"Pcic.constr_of_prog: Translation cc_term -> rawconstr..."; 
-       'fNL >];
+    (fnl () ++ str"Pcic.constr_of_prog: Translation cc_term -> rawconstr..." ++ 
+       fnl ());
   let r = Pcic.rawconstr_of_prog cc in
   deb_mess (Printer.pr_rawterm r);
 
   (* 6. résolution implicites *)
-  deb_mess [< 'fNL; 'sTR"Resolution implicits (? => Meta(n))..."; 'fNL >];
+  deb_mess (fnl () ++ str"Resolution implicits (? => Meta(n))..." ++ fnl ());
   let oc = understand_gen_tcc Evd.empty (Global.env()) [] [] None r in
   deb_mess (Printer.prterm (snd oc));
 
@@ -227,9 +227,9 @@ let correctness s p opttac =
   start_proof id Declare.NeverDischarge sign cty;
   Penv.new_edited id (v,p);
   if !debug then show_open_subgoals();
-  deb_mess [< 'sTR"Pred.red_cci: Reduction..."; 'fNL >];
+  deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ());
   let oc = reduce_open_constr oc in
-  deb_mess [< 'sTR"AFTER REDUCTION:"; 'fNL >];
+  deb_mess (str"AFTER REDUCTION:" ++ fnl ());
   deb_mess (Printer.prterm (snd oc));
   let tac = (tclTHEN (Refine.refine_tac oc) automatic) in
   let tac = match opttac with 
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml
index 2e95f840f2..a6f7a0ae95 100644
--- a/contrib/correctness/ptyping.ml
+++ b/contrib/correctness/ptyping.ml
@@ -529,7 +529,7 @@ let rec states_desc ren env loc = function
 	if s_e.info.kappa = c then
 	  s_e
       	else begin
-	  if !verbose_fix then begin mSGNL (pp_type_c s_e.info.kappa) end ;
+	  if !verbose_fix then begin msgnl (pp_type_c s_e.info.kappa) end ;
 	  state_rec s_e.info.kappa
       	end
       in 
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index 5e454a2520..dbb903ab1e 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -235,70 +235,70 @@ open Util
 open Printer
 
 let pp_pre = function
-    [] -> [< >]
+    [] -> (mt ())
   | l  ->
-      hOV 0 [< 'sTR"pre "; 
-	       prlist_with_sep (fun () -> [< 'sPC >]) 
-		 (fun x -> prterm x.p_value) l >]
+      hov 0 (str"pre " ++ 
+	       prlist_with_sep (fun () -> (spc ())) 
+		 (fun x -> prterm x.p_value) l)
 
 let pp_post = function
-    None -> [< >]
-  | Some c -> hOV 0 [< 'sTR"post "; prterm c.a_value >]
+    None -> (mt ())
+  | Some c -> hov 0 (str"post " ++ prterm c.a_value)
 
 let rec pp_type_v = function
-    Ref v -> hOV 0 [< pp_type_v v; 'sPC; 'sTR"ref" >]
-  | Array (cc,v) -> hOV 0 [< 'sTR"array "; prterm cc; 'sTR" of "; pp_type_v v >]
+    Ref v -> hov 0 (pp_type_v v ++ spc () ++ str"ref")
+  | Array (cc,v) -> hov 0 (str"array " ++ prterm cc ++ str" of " ++ pp_type_v v)
   | Arrow (b,c) -> 
-      hOV 0 [< prlist_with_sep (fun () -> [< >]) pp_binder b; 
-	       pp_type_c c >]
+      hov 0 (prlist_with_sep (fun () -> (mt ())) pp_binder b ++ 
+	       pp_type_c c)
   | TypePure c -> prterm c
 
 and pp_type_c ((id,v),e,p,q) =
-  hOV 0 [< 'sTR"returns "; pr_id id; 'sTR":"; pp_type_v v; 'sPC; 
-	   Peffect.pp e; 'sPC; pp_pre p; 'sPC; pp_post q ;
-	   'sPC; 'sTR"end" >]
+  hov 0 (str"returns " ++ pr_id id ++ str":" ++ pp_type_v v ++ spc () ++ 
+	   Peffect.pp e ++ spc () ++ pp_pre p ++ spc () ++ pp_post q ++
+	   spc () ++ str"end")
 
 and pp_binder = function
-    id,BindType v -> [< 'sTR"("; pr_id id; 'sTR":"; pp_type_v v; 'sTR")" >]
-  | id,BindSet -> [< 'sTR"("; pr_id id; 'sTR":Set)" >]
-  | id,Untyped -> [< 'sTR"("; pr_id id; 'sTR")" >]
+    id,BindType v -> (str"(" ++ pr_id id ++ str":" ++ pp_type_v v ++ str")")
+  | id,BindSet -> (str"(" ++ pr_id id ++ str":Set)")
+  | id,Untyped -> (str"(" ++ pr_id id ++ str")")
 
 (* pretty-print of cc-terms (intermediate terms) *)
 
 let rec pp_cc_term = function
     CC_var id -> pr_id id
   | CC_letin (_,_,bl,c,c1) ->
-      hOV 0 [< hOV 2 [< 'sTR"let ";
-		  	prlist_with_sep (fun () -> [< 'sTR"," >])
-			  (fun (id,_) -> pr_id id) bl;
-		  	'sTR" ="; 'sPC;
-		  	pp_cc_term c;
-		  	'sTR " in">];
-	       'fNL;
-	       pp_cc_term c1 >]
+      hov 0 (hov 2 (str"let " ++
+		  	prlist_with_sep (fun () -> (str","))
+			  (fun (id,_) -> pr_id id) bl ++
+		  	str" =" ++ spc () ++
+		  	pp_cc_term c ++
+		  	str " in") ++
+	       fnl () ++
+	       pp_cc_term c1)
   | CC_lam (bl,c) ->
-      hOV 2 [< prlist (fun (id,_) -> [< 'sTR"["; pr_id id; 'sTR"]" >]) bl;
-	       'cUT;
-	       pp_cc_term c >]
+      hov 2 (prlist (fun (id,_) -> (str"[" ++ pr_id id ++ str"]")) bl ++
+	       cut () ++
+	       pp_cc_term c)
   | CC_app (f,args) ->
-      hOV 2 [< 'sTR"("; 
-	       pp_cc_term f; 'sPC;
-	       prlist_with_sep (fun () -> [< 'sPC >]) pp_cc_term args;
-	       'sTR")" >]
+      hov 2 (str"(" ++ 
+	       pp_cc_term f ++ spc () ++
+	       prlist_with_sep (fun () -> (spc ())) pp_cc_term args ++
+	       str")")
   | CC_tuple (_,_,cl) ->
-      hOV 2 [< 'sTR"(";
-	       prlist_with_sep (fun () -> [< 'sTR","; 'cUT >])
-		 pp_cc_term cl;
-	       'sTR")" >]
+      hov 2 (str"(" ++
+	       prlist_with_sep (fun () -> (str"," ++ cut ()))
+		 pp_cc_term cl ++
+	       str")")
   | CC_case (_,b,[e1;e2]) ->
-      hOV 0 [< 'sTR"if "; pp_cc_term b; 'sTR" then"; 'fNL;
-	       'sTR"  "; hOV 0 (pp_cc_term e1); 'fNL;
-	       'sTR"else"; 'fNL;
-	       'sTR"  "; hOV 0 (pp_cc_term e2) >]
+      hov 0 (str"if " ++ pp_cc_term b ++ str" then" ++ fnl () ++
+	       str"  " ++ hov 0 (pp_cc_term e1) ++ fnl () ++
+	       str"else" ++ fnl () ++
+	       str"  " ++ hov 0 (pp_cc_term e2))
   | CC_case _ ->
-      hOV 0 [< 'sTR"<Case: not yet implemented>" >]
+      hov 0 (str"<Case: not yet implemented>")
   | CC_expr c ->
-      hOV 0 (prterm c)
+      hov 0 (prterm c)
   | CC_hole c ->
-      [< 'sTR"(?::"; prterm c; 'sTR")" >]
+      (str"(?::" ++ prterm c ++ str")")
 
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 9b111bbf43..9467986ef8 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 8ce82a45b0..ce367c1c2b 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 132367de95..b9a43fd040 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 8d5cf6ebe1..499503f171 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 32ad5053ba..53408461f5 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 778683646d..36ccff88d1 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 8c8138fd09..a45490f201 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"
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index eae99993f6..00db51adf7 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -54,11 +54,11 @@ set_flags := (function () ->
                   (g_nat_syntax_flag := true; ())
                 else ());;
 
-let guarded_force_eval_stream s = 
+let guarded_force_eval_stream (s : std_ppcmds) = 
   let l = ref [] in
   let f elt = l:= elt :: !l in 
   (try  Stream.iter f s with
-  | _ -> f (sTR "error guarded_force_eval_stream"));
+  | _ -> f (Stream.next (str "error guarded_force_eval_stream")));
   Stream.of_list (List.rev !l);;
 
 
@@ -67,7 +67,7 @@ let rec string_of_path p =
               | i::p -> (string_of_int i)^" "^ (string_of_path p)
 ;;
 let print_path p =
-    output_results_nl [< 'sTR "Path:"; 'sTR  (string_of_path p)>]
+    output_results_nl (str "Path:" ++ str (string_of_path p))
 ;;
 
 let kill_proof_node index =
@@ -83,7 +83,8 @@ let kill_proof_node index =
 (*Message functions, the text of these messages is recognized by the protocols *)
 (*of CtCoq                                                                     *)
 let ctf_header message_name request_id =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR message_name; 'fNL; 'iNT request_id; 'fNL >];;
+  fnl () ++ str "message" ++ fnl () ++ str message_name ++ fnl () ++ 
+  int request_id ++ fnl ();;
 
 let ctf_acknowledge_command request_id command_count opt_exn =
   let goal_count, goal_index = 
@@ -94,14 +95,14 @@ let ctf_acknowledge_command request_id command_count opt_exn =
         g_count, (min g_count !current_goal_index)
     else
       (0, 0) in
-  [< ctf_header "acknowledge" request_id;
-     'iNT command_count; 'fNL; 
-    'iNT goal_count; 'fNL; 
-    'iNT goal_index; 'fNL; 
-    'sTR !current_proof_name; 'fNL;
-    (match opt_exn with
-      Some e -> Errors.explain_exn e
-    | None -> [< >]); 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+  (ctf_header "acknowledge" request_id ++
+   int command_count ++ fnl () ++ 
+   int goal_count ++ fnl () ++ 
+   int goal_index ++ fnl () ++ 
+   str !current_proof_name ++ fnl () ++
+   (match opt_exn with
+	Some e -> Errors.explain_exn e
+      | None -> mt ()) ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
 
 let ctf_undoResults = ctf_header "undo_results";;
 
@@ -116,35 +117,37 @@ let ctf_Location = ctf_header "location";;
 let ctf_StateMessage = ctf_header "state";;
 
 let ctf_PathGoalMessage () =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "single_goal"; 'fNL >];;
+  fnl () ++ str "message" ++ fnl () ++ str "single_goal" ++ fnl ();;
 
 let ctf_GoalReqIdMessage = ctf_header "single_goal_state";;
 
 let ctf_NewStateMessage = ctf_header "fresh_state";;
 
-let ctf_SavedMessage () = [< 'fNL; 'sTR "message"; 'fNL; 'sTR "saved"; 'fNL >];;
+let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++ str "saved" ++ fnl ();;
 
 let ctf_KilledMessage req_id ngoals =
- [< ctf_header "killed" req_id; 'iNT ngoals; 'fNL >];;
+ ctf_header "killed" req_id ++ int ngoals ++ fnl ();;
 
 let ctf_AbortedAllMessage () =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "aborted_all"; 'fNL >];;
+ fnl () ++ str "message" ++ fnl () ++ str "aborted_all" ++ fnl ();;
 
 let ctf_AbortedMessage request_id na =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "aborted_proof"; 'fNL; 'iNT request_id; 'fNL;
- 'sTR na; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+  fnl () ++ str "message" ++ fnl () ++ str "aborted_proof" ++ fnl () ++ 
+  int request_id ++ fnl () ++
+  str na ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
 
 let ctf_UserErrorMessage request_id stream =
- let stream = guarded_force_eval_stream stream in
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "user_error"; 'fNL; 'iNT request_id; 'fNL;
-  stream; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+  let stream = guarded_force_eval_stream stream in
+  fnl () ++ str "message" ++ fnl () ++ str "user_error" ++ fnl () ++ 
+  int request_id ++ fnl () ++
+  stream ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
 
 let ctf_ResetInitialMessage () =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "reset_initial"; 'fNL >];;
+  fnl () ++ str "message" ++ fnl () ++ str "reset_initial" ++ fnl ();;
 
-let ctf_ResetIdentMessage request_id str =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "reset_ident"; 'fNL; 'iNT request_id; 'fNL;
- 'sTR str; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+let ctf_ResetIdentMessage request_id s =
+  fnl () ++ str "message" ++ fnl () ++ str "reset_ident" ++ fnl () ++ int request_id ++ fnl () ++
+  str s ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
 
 type vtp_tree =
   | P_rl of ct_RULE_LIST
@@ -175,7 +178,7 @@ let break_happened = ref false;;
 let output_results stream vtp_tree =
     let _ = Sys.signal Sys.sigint
        (Sys.Signal_handle(fun i -> (break_happened := true;()))) in
-    mSG stream;
+    msg stream;
     match vtp_tree with
       Some t -> print_tree t
     | None -> ();;
@@ -184,7 +187,7 @@ let output_results_nl stream =
     let _ = Sys.signal Sys.sigint
        (Sys.Signal_handle(fun i -> break_happened := true;()))
     in
-    mSGNL stream;;
+    msgnl stream;;
 
 
 let rearm_break () =
@@ -216,7 +219,7 @@ let show_nth n =
   try
     let pf = proof_of_pftreestate (get_pftreestate()) in
     if (!text_proof_flag<>"off") then
-(*      errorlabstrm "debug" [< 'sTR "text printing unplugged" >]*)
+(*      errorlabstrm "debug" [< str "text printing unplugged" >]*)
        (if n=0
 	   then output_results (ctf_TextMessage !global_request_id)
                                (Some (P_text (show_proof !text_proof_flag [])))
@@ -255,14 +258,14 @@ let add_search (global_reference:global_reference) assumptions cstr =
                   CT_coerce_ID_to_FORMULA(
                     CT_ident ("Error printing" ^ id_string))) in
     ctv_SEARCH_LIST:= ast::!ctv_SEARCH_LIST
-  with e -> mSGNL [< 'sTR "add_search raised an exception" >]; raise e;;
+  with e -> msgnl (str "add_search raised an exception"); raise e;;
 
 let make_error_stream node_string =
- [< 'sTR "The syntax of "; 'sTR node_string;
- 'sTR " is inconsistent with the vernac interpreter entry" >];;
+  str "The syntax of " ++ str node_string ++
+  str " is inconsistent with the vernac interpreter entry";;
 
 let ctf_EmptyGoalMessage id =
- [< 'fNL; 'sTR "Empty Goal is a no-op.  Fun oh fun."; 'fNL >];;
+  fnl () ++ str "Empty Goal is a no-op.  Fun oh fun." ++ fnl ();;
 
 
 let print_check (ast, judg) =
@@ -271,15 +274,17 @@ let print_check (ast, judg) =
      (try translate_constr (Global.env()) value 
       with UserError(f,str) ->
            raise(UserError(f,
-			   [< Ast.print_ast 
-				(ast_of_constr true (Global.env()) value);
-			      'fNL; str >]))) in
+			   Ast.print_ast 
+			     (ast_of_constr true (Global.env()) value) ++
+			   fnl () ++ str))) 
+ in
  let type_ct_ast =
      (try translate_constr (Global.env()) typ
       with UserError(f,str) ->
-           raise(UserError(f, [< Ast.print_ast (ast_of_constr true (Global.env())
-					       value);
-				 'fNL; str >]))) in
+           raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env())
+					       value) ++
+				 fnl () ++ str))) 
+ in
  ((ctf_SearchResults !global_request_id),
  (Some  (P_pl
   (CT_premises_list
@@ -318,16 +323,16 @@ let globcv = function
 let pbp_tac_pcoq =
     pbp_tac (function x -> 
       output_results
-  	[< 'fNL; 'sTR "message"; 'fNL; 'sTR "pbp_results"; 'fNL;
-	  'iNT !global_request_id;  'fNL>]
-       (Some (P_t(xlate_tactic x))));;
+  	(fnl () ++ str "message" ++ fnl () ++ str "pbp_results" ++ fnl () ++
+	 int !global_request_id ++  fnl ())
+	(Some (P_t(xlate_tactic x))));;
 
 
 let dad_tac_pcoq =
   dad_tac(function x -> 
     output_results
-    [< 'fNL; 'sTR "message"; 'fNL; 'sTR "pbp_results"; 'fNL;
-       'iNT !global_request_id;  'fNL >]
+    (fnl () ++ str "message" ++ fnl () ++ str "pbp_results" ++ fnl () ++
+       int !global_request_id ++  fnl ())
     (Some (P_t(xlate_tactic x))));;
 
 let search_output_results () =
@@ -346,8 +351,8 @@ let debug_tac2_pcoq = function
 	try
 	  let result = report_error ast the_goal the_ast the_path [] g in
 	  (errorlabstrm "DEBUG TACTIC"
-	    [< 'sTR "no error here "; 'fNL; pr_goal (sig_it g);
-	      'fNL; 'sTR "the tactic is"; 'fNL ; Printer.gentacpr ast >];
+	    (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++
+	     fnl () ++ str "the tactic is" ++ fnl ()  ++ Printer.gentacpr ast);
 	   result)
 	with
 	  e ->
@@ -481,9 +486,9 @@ let command_changes = [
 	    begin
 	      if kind = "LETTOP" && not(refining ()) then
 		errorlabstrm "StartProof"
-		  [< 'sTR
-                       "Let declarations can only be used in proof editing mode"
-		  >];
+		  (str
+                     "Let declarations can only be used in proof editing mode"
+		  );
 		let str = (string_of_id s) in
 		start_proof_com (Some s) stre c;
 		History.start_proof str;
@@ -563,7 +568,7 @@ let command_changes = [
 	 (function
 	     () ->
 	       errorlabstrm "Begin Silent" 
-		 [< 'sTR "not available in Centaur mode" >])
+		 (str "not available in Centaur mode"))
      | _ -> errorlabstrm "BeginSilent" (make_error_stream "BeginSilent")));
   
   ("EndSilent", 
@@ -572,7 +577,7 @@ let command_changes = [
 	 (function
 	     () ->
 	       errorlabstrm "End Silent"
-		 [< 'sTR "not available in Centaur mode" >])
+		 (str "not available in Centaur mode"))
      | _ -> errorlabstrm "EndSilent" (make_error_stream "EndSilent")));
   
   ("ABORT", 
@@ -633,7 +638,7 @@ let command_changes = [
 	 (function () -> 
 	   let results = xlate_vernac_list (Ctast.ast_to_ct (name_to_ast qid)) in
 	   output_results 
-	     [<'fNL; 'sTR "message"; 'fNL; 'sTR "PRINT_VALUE"; 'fNL >]
+	     (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl ())
 	     (Some (P_cl results)))
      | _ -> errorlabstrm "PrintId" (make_error_stream "PrintId")));
   
@@ -646,7 +651,7 @@ let command_changes = [
 	   match kind with
 	   | "CHECK" -> print_check
 	   | "PRINTTYPE" ->
-	       errorlabstrm "PrintType" [< 'sTR "Not yet supported in CtCoq" >]
+	       errorlabstrm "PrintType" (str "Not yet supported in CtCoq")
 	   | _ -> errorlabstrm "CHECK" (make_error_stream "CHECK") in
 	 (function () -> 
 	   let a,b = f (c, judgment_of_rawconstr evmap env c) in
@@ -692,8 +697,8 @@ let command_changes = [
 	 (fun () -> 
 	   let results = dad_rule_names() in
 	   output_results
-	     [< 'fNL; 'sTR "message"; 'fNL; 'sTR "dad_rule_names"; 'fNL;
-	       'iNT !global_request_id; 'fNL >]
+	     (fnl () ++ str "message" ++ fnl () ++ str "dad_rule_names" ++ fnl () ++
+	      int !global_request_id ++ fnl ())
 	     (Some (P_ids
 		      (CT_id_list
 			 (List.map (fun s -> CT_ident s) results)))))
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 7f2ea95a4f..ce38174044 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -254,7 +254,7 @@ vinterp_add "AddDadRule"
               let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in
               (add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr (Ctast.ast_to_ct com)))
             | _ -> errorlabstrm "AddDadRule1"
-                    [< 'sTR "AddDadRule2">]);
+                    [< str "AddDadRule2">]);
 add_dad_rule "distributivity-inv"
 (Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])]))
 [2; 2]
diff --git a/contrib/interface/debug_tac.ml b/contrib/interface/debug_tac.ml
index b7542fa745..80d9d72018 100644
--- a/contrib/interface/debug_tac.ml
+++ b/contrib/interface/debug_tac.ml
@@ -183,7 +183,7 @@ and checked_thens: report_holder -> Coqast.t -> Coqast.t list -> tactic =
 	  | Recursive_fail tr -> Tree_fail tr
 	  | Fail -> Failed 1
 	  | _ -> errorlabstrm "check_thens"
-                  [< 'sTR "this case should not happen in check_thens">])::
+                  (str "this case should not happen in check_thens"))::
 	  !report_holder);
       result)
 
@@ -297,8 +297,8 @@ let rec reconstruct_success_tac ast =
 	| _ ->
 	    errorlabstrm
 	      "this error case should not happen on an unknown tactic"
-              [< 'sTR "error in reconstruction with "; 'fNL;
-		(gentacpr ast) >]);;
+              (str "error in reconstruction with " ++ fnl () ++
+	       (gentacpr ast)));;
 	  
 
 let rec path_to_first_error = function
@@ -332,15 +332,16 @@ let debug_tac = function
       	let clean_ast = expand_tactic ast in
       	let report_tree =
           try List.hd !report with
-	    Failure "hd" -> (mSGNL [< 'sTR "report is empty" >]; Failed 1) in
+	    Failure "hd" -> (msgnl (str "report is empty"); Failed 1) in
       	let success_tac = 
 	  reconstruct_success_tac clean_ast report_tree in
         let compact_success_tac =
 	  flatten_then success_tac in
-      	mSGNL [< 'fNL; 'sTR "=========    Successful tactic    ============="; 
-                 'fNL;
-	      	gentacpr compact_success_tac; 'fNL;
-	      	'sTR "========= End of successful tactic ============">];
+      	msgnl (fnl () ++
+	       str "=========    Successful tactic    =============" ++
+               fnl () ++
+	       gentacpr compact_success_tac ++ fnl () ++
+	       str "========= End of successful tactic ============");
       	result)
   | _ -> error "wrong arguments for debug_tac";;
 
@@ -427,10 +428,9 @@ let rec report_error
 	    with
 	      e ->
 		if !the_count > 1 then
-		  mSGNL
-		    [< 'sTR "in branch no "; 'iNT !the_count; 
-		      'sTR " after tactic ";
-		      gentacpr a >];
+		  msgnl
+		    (str "in branch no " ++ int !the_count ++
+		     str " after tactic " ++ gentacpr a);
 		raise e)
     | Node(_, "TACTICLIST", a::b::c::tl) ->
 	report_error (ope("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl))
@@ -458,16 +458,16 @@ let descr_first_error = function
 	let the_path = ref ([] : int list) in
 	try
 	  let result = report_error ast the_goal the_ast the_path [] g in
-	  mSGNL [< 'sTR "no Error here" >];
+	  msgnl (str "no Error here");
 	  result
 	with
 	  e ->
-	    (mSGNL [< 'sTR "Execution of this tactic raised message " ; 'fNL;
-		     'fNL; Errors.explain_exn e; 'fNL;
-		     'fNL; 'sTR "on goal" ; 'fNL;
-		     pr_goal (sig_it (strip_some !the_goal)); 'fNL;
-		     'sTR "faulty tactic is"; 'fNL; 'fNL;
-		     gentacpr (flatten_then !the_ast); 'fNL >];
+	    (msgnl (str "Execution of this tactic raised message " ++ fnl () ++
+		    fnl () ++ Errors.explain_exn e ++ fnl () ++
+		    fnl () ++ str "on goal"  ++ fnl () ++
+		    pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++
+		    str "faulty tactic is" ++ fnl () ++ fnl () ++
+		    gentacpr (flatten_then !the_ast) ++ fnl ());
 	     tclIDTAC g))
   | _ -> error "wrong arguments for descr_first_error";;
 
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index e961063689..a7d5644f0a 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -56,8 +56,8 @@ let impl_args_to_string = function
 let implicit_args_id_to_ast_list id l ast_list = 
     (match impl_args_to_string l with
            None -> ast_list
-         | Some(s) -> (str("For " ^ (string_of_id id)))::
-                       (str s)::
+         | Some(s) -> (string ("For " ^ (string_of_id id)))::
+                      (string s)::
                        ast_list);;
 
 (* This function construct an ast to enumerate the implicit positions for an
@@ -125,7 +125,7 @@ let mutual_to_ast_list sp mib =
     Array.fold_right
       (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
   (ope("MUTUALINDUCTIVE",
-	  [str (if mib.mind_finite then "Inductive" else "CoInductive");
+	  [string (if mib.mind_finite then "Inductive" else "CoInductive");
 	  ope("VERNACARGLIST", ast_list)])::
      (implicit_args_to_ast_list sp mipv));;
 
@@ -135,11 +135,11 @@ let constr_to_ast v =
 let implicits_to_ast_list implicits =
     (match (impl_args_to_string implicits) with
                   None -> []
-                | Some s -> [ope("COMMENT", [str s])]);;
+                | Some s -> [ope("COMMENT", [string s])]);;
 
 let make_variable_ast name typ implicits =
    (ope("VARIABLE",
-    [str "VARIABLE";
+    [string "VARIABLE";
      ope("BINDERLIST",
          [ope("BINDER",
             [(constr_to_ast (body_of_type typ));
@@ -148,7 +148,7 @@ let make_variable_ast name typ implicits =
     
 let make_definition_ast name c typ implicits =
  (ope("DEFINITION",
-      [str "DEFINITION";
+      [string "DEFINITION";
        nvar name;
        ope("COMMAND",
            [ope("CAST",
@@ -193,8 +193,8 @@ let leaf_entry_to_ast_list (sp,lobj) =
   | (_, "INDUCTIVE") -> inductive_to_ast_list sp
   | (_, s) -> 
       errorlabstrm 
-      	"print" [< 'sTR ("printing of unrecognized object " ^
-			 s ^ " has been required") >];;
+      	"print" (str ("printing of unrecognized object " ^
+		      s ^ " has been required"));;
 
 
 
@@ -232,10 +232,11 @@ let name_to_ast (qid:Nametab.qualid) =
 	    try
 	      let sp = Syntax_def.locate_syntactic_definition qid in
 		errorlabstrm "print"
-      		  [< 'sTR "printing of syntax definitions not implemented" >]
+      		  (str "printing of syntax definitions not implemented")
 	    with Not_found ->
 	      errorlabstrm "print"
-		[< Nametab.pr_qualid qid;
-		   'sPC; 'sTR "not a defined object" >] in
-    ope("vernac_list", l);;
+		(Nametab.pr_qualid qid ++
+		 spc () ++ str "not a defined object")
+  in
+  ope("vernac_list", l);;
 
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 6b2e388738..fad5c1e341 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -2,10 +2,10 @@ open Util;;
 
 open System;;
 
-open Pp;;
-
 open Ctast;;
 
+open Pp;;
+
 open Library;;
 
 open Ascent;;
@@ -43,15 +43,15 @@ let print_parse_results n msg =
   flush stdout;;
 
 let ctf_SyntaxErrorMessage reqid pps =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "syntax_error"; 'fNL; 'iNT reqid; 'fNL;
-   pps; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+ (fnl () ++ str "message" ++ fnl () ++ str "syntax_error" ++ fnl () ++ int reqid ++ fnl () ++
+   pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
 let ctf_SyntaxWarningMessage reqid pps =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "syntax_warning"; 'fNL; 'iNT reqid; 'fNL;
-   pps; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+ (fnl () ++ str "message" ++ fnl () ++ str "syntax_warning" ++ fnl () ++ int reqid ++ fnl () ++
+   pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
 
 let ctf_FileErrorMessage reqid pps =
- [< 'fNL; 'sTR "message"; 'fNL; 'sTR "file_error"; 'fNL; 'iNT reqid; 'fNL;
-   pps; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];;
+ (fnl () ++ str "message" ++ fnl () ++ str "file_error" ++ fnl () ++ int reqid ++ fnl () ++
+   pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
 
 (*In the code for CoqV6.2, the require_module call is encapsulated in
   a function "without_mes_ambig".  Here I have supposed that this
@@ -60,7 +60,7 @@ let try_require_module import specif name fname =
  try Library.require_module (if specif = "UNSPECIFIED" then None
   else Some (specif = "SPECIFICATION")) (Nametab.make_short_qualid (Names.id_of_string name)) fname (import = "IMPORT")
  with
- | e -> mSGNL [< 'sTR "Reinterning of "; 'sTR name; 'sTR " failed" >];;
+ | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");;
 
 let execute_when_necessary ast =
  (match ast with
@@ -79,11 +79,12 @@ let execute_when_necessary ast =
   | _ -> ()); ast;;
 
 let parse_to_dot =
-  let rec dot = parser
-      [< '("", ".") >] -> ()
-    | [< '("EOI", "") >] -> raise End_of_file
-    | [< '_; s >] -> dot s
-  in Gram.Entry.of_parser "Coqtoplevel.dot" dot;;
+  let rec dot st = match Stream.next st with
+    | ("", ".") -> ()
+    | ("EOI", "") -> raise End_of_file
+    | _ -> dot st
+  in 
+  Gram.Entry.of_parser "Coqtoplevel.dot" dot;;
 
 let rec discard_to_dot stream =
   try Gram.Entry.parse parse_to_dot (Gram.parsable stream) with
@@ -149,11 +150,11 @@ let parse_command_list reqid stream string_list =
         with
         | (Stdpp.Exc_located(l, Stream.Error txt)) as e -> 
           begin
-             mSGNL (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e));
+             msgnl (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e));
              try
                 discard_to_dot stream;
-                mSGNL [< 'sTR "debug"; 'fNL; 'iNT this_pos; 'fNL; 'iNT 
-                  (Stream.count stream) >];
+                msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++ int 
+                  (Stream.count stream));
                 Some( Node(l, "PARSING_ERROR",
                         List.map Ctast.str
                         (get_substring_list string_list this_pos
@@ -175,7 +176,7 @@ let parse_command_list reqid stream string_list =
     | None -> [] in
     match parse_whole_stream () with
     | first_one::tail -> (P_cl (CT_command_list(first_one, tail)))
-    | [] -> raise (UserError ("parse_string", [< 'sTR "empty text." >]));;
+    | [] -> raise (UserError ("parse_string", (str "empty text.")));;
 
 (*When parsing a string using a phylum, the string is first transformed
   into a Coq Ast using the regular Coq parser, then it is transformed into
@@ -215,12 +216,12 @@ let parse_string_action reqid phylum char_stream string_list =
  with
  | Stdpp.Exc_located(l,Match_failure(_,_,_)) ->
     flush_until_end_of_stream char_stream;
-    mSGNL (ctf_SyntaxErrorMessage reqid
+    msgnl (ctf_SyntaxErrorMessage reqid
               (Errors.explain_exn 
                  (Stdpp.Exc_located(l,Stream.Error "match failure"))))
  | e ->
     flush_until_end_of_stream char_stream;
-    mSGNL (ctf_SyntaxErrorMessage reqid (Errors.explain_exn e));;
+    msgnl (ctf_SyntaxErrorMessage reqid (Errors.explain_exn e));;
 
 
 let quiet_parse_string_action char_stream =
@@ -247,10 +248,10 @@ let parse_file_action reqid file_name =
                 this_ast
               with
             | Stdpp.Exc_located(l,Stream.Error txt ) -> 
-                 mSGNL (ctf_SyntaxWarningMessage reqid
-                [< 'sTR "Error with file"; 'sPC; 'sTR file_name; 'fNL;
+                 msgnl (ctf_SyntaxWarningMessage reqid
+                (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++
                    Errors.explain_exn 
-                      (Stdpp.Exc_located(l,Stream.Error txt)) >]);
+                      (Stdpp.Exc_located(l,Stream.Error txt))));
                  let rec discard_to_dot () =
                  try Gram.Entry.parse parse_to_dot (Gram.parsable stream)
                  with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot()
@@ -276,18 +277,18 @@ let parse_file_action reqid file_name =
       | first_one :: tail ->
        print_parse_results reqid
           (P_cl (CT_command_list (first_one, tail)))
-      | [] -> raise (UserError ("parse_file_action", [< 'sTR "empty file." >]))
+      | [] -> raise (UserError ("parse_file_action", (str "empty file.")))
  with
  | Stdpp.Exc_located(l,Match_failure(_,_,_)) ->
- mSGNL
+ msgnl
   (ctf_SyntaxErrorMessage reqid
-  [< 'sTR "Error with file"; 'sPC; 'sTR file_name; 'fNL;
-  Errors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure")) >])
+  (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++
+  Errors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure"))))
  | e ->
- mSGNL
+ msgnl
   (ctf_SyntaxErrorMessage reqid
-  [< 'sTR "Error with file"; 'sPC; 'sTR file_name; 'fNL;
-  Errors.explain_exn e >]);;
+  (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++
+  Errors.explain_exn e));;
 
 (* This function is taken from Mltop.add_path *)
 
@@ -297,7 +298,7 @@ let add_path dir coq_dirpath =
       Library.add_load_path_entry (dir,coq_dirpath)
     end
   else
-    wARNING [< 'sTR ("Cannot open " ^ dir) >]
+    msg_warning (str ("Cannot open " ^ dir))
 
 let convert_string d =
   try Names.id_of_string d
@@ -315,7 +316,7 @@ let add_rec_path dir coq_dirpath =
       List.iter Library.add_load_path_entry dirs
     end
     else
-      wARNING [< 'sTR ("Cannot open " ^ dir) >];;
+      msg_warning (str ("Cannot open " ^ dir));;
 
 let add_path_action reqid string_arg =
   let directory_name = glob string_arg in
@@ -325,30 +326,30 @@ let add_path_action reqid string_arg =
     end;;
 
 let print_version_action () =
-  mSGNL [< >];
-  mSGNL [< 'sTR "$Id$" >];;
+  msgnl (mt ());
+  msgnl (str "$Id$");;
 
 let load_syntax_action reqid module_name =
- mSG [< 'sTR "loading "; 'sTR module_name; 'sTR "... " >];
+ msg (str "loading " ++ str module_name ++ str "... ");
  try
       (let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in
       read_module qid;
-      mSG [< 'sTR "opening... ">];
+      msg (str "opening... ");
       let fullname = Nametab.locate_loaded_library qid in 
       import_module fullname; 
-      mSGNL [< 'sTR "done"; 'fNL >];
+      msgnl (str "done" ++ fnl ());
       ())
  with
  | UserError (label, pp_stream) ->
  (*This one may be necessary to make sure that the message won't be indented *)
- mSGNL [< >];
- mSGNL
-  [< 'fNL; 'sTR "error while loading syntax module "; 'sTR module_name;
-  'sTR ": "; 'sTR label; 'fNL; pp_stream >]
+ msgnl (mt ());
+ msgnl
+  (fnl () ++ str "error while loading syntax module " ++ str module_name ++
+  str ": " ++ str label ++ fnl () ++ pp_stream)
  | e ->
-  mSGNL [< >];
-  mSGNL
-   [< 'fNL; 'sTR "message"; 'fNL; 'sTR "load_error"; 'fNL; 'iNT reqid; 'fNL >];
+  msgnl (mt ());
+  msgnl
+   (fnl () ++ str "message" ++ fnl () ++ str "load_error" ++ fnl () ++ int reqid ++ fnl ());
   ();;
 
 let coqparser_loop inchan =
@@ -370,12 +371,12 @@ Libobject.relax true;
        if Sys.file_exists coqdir then
 	 coqdir
        else
-	 (mSGNL [< 'sTR "could not find the value of COQDIR" >]; exit 1) in
+	 (msgnl (str "could not find the value of COQDIR"); exit 1) in
      begin
        add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nameops.coq_root]);
        add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nameops.coq_root]);
        add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nameops.coq_root]);
-       List.iter (fun a -> mSGNL [< 'sTR a >]) (get_load_path())
+       List.iter (fun a -> msgnl (str a)) (get_load_path())
      end;
 (try 
   (match create_entry (get_univ "nat") "number" ETast with
@@ -387,10 +388,10 @@ Libobject.relax true;
 	    (fun s loc ->
 		 Node((0,0),"XTRA",[Str((0,0),"omega_integer_for_ctcoq");
 				 Num((0,0),int_of_string s)]))]]
-   | _ -> mSGNL [< 'sTR "unpredicted behavior of Grammar.extend" >])
+   | _ -> msgnl (str "unpredicted behavior of Grammar.extend"))
 
  with
-   e -> mSGNL [< 'sTR "could not add a parser for numbers" >]);
+   e -> msgnl (str "could not add a parser for numbers"));
 (let vernacrc =
    try
      Sys.getenv "VERNACRC"
@@ -406,28 +407,28 @@ Libobject.relax true;
    with
      | End_of_file -> ()
      | e ->
-	 (mSGNL (Errors.explain_exn e);
-	  mSGNL [< 'sTR "could not load the VERNACRC file" >]);
+	 (msgnl (Errors.explain_exn e);
+	  msgnl (str "could not load the VERNACRC file"));
 	 try
-	   mSGNL [< 'sTR vernacrc >]
+	   msgnl (str vernacrc)
 	 with
 	     e -> ());
 (try let user_vernacrc =
    try Some(Sys.getenv "USERVERNACRC")
    with
      | Not_found as e ->
-	 mSGNL [< 'sTR "no .vernacrc file" >]; None in
+	 msgnl (str "no .vernacrc file"); None in
    (match user_vernacrc with
       	Some f -> coqparser_loop (open_in f)
       | None -> ())
  with
    | End_of_file -> ()
    | e ->
-       mSGNL (Errors.explain_exn e);
-       mSGNL [< 'sTR "error in your .vernacrc file" >]);
-mSGNL [< 'sTR "Starting Centaur Specialized Parser Loop" >];
+       msgnl (Errors.explain_exn e);
+       msgnl (str "error in your .vernacrc file"));
+msgnl (str "Starting Centaur Specialized Parser Loop");
 try
   coqparser_loop stdin
 with 
   | End_of_file -> ()
-  | e -> mSGNL(Errors.explain_exn e))
+  | e -> msgnl(Errors.explain_exn e))
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 5bfad2f52c..c23394e8c7 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1806,7 +1806,7 @@ let show_proof lang gpath =
     ;;
 
 let show_nproof path =
-  pP (sp_print (sph [spi; show_proof "fr" path]));;
+  pp (sp_print (sph [spi; show_proof "fr" path]));;
 
 vinterp_add "ShowNaturalProof"
 	    (fun _ ->
diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml
index e3bca22433..b689620e34 100644
--- a/contrib/interface/showproof_ct.ml
+++ b/contrib/interface/showproof_ct.ml
@@ -120,31 +120,31 @@ let sphv l =
 
 let rec prlist_with_sep f g l =
     match l with 
-      [] -> hOV 0 [< >]
-     |x::l1 -> hOV 0 [< (g x); (f ()); (prlist_with_sep f g l1)>]
+      [] -> hov 0 (mt ())
+     |x::l1 -> hov 0 ((g x) ++ (f ()) ++ (prlist_with_sep f g l1))
 ;;
    
 let rec sp_print x = 
    match x with
-     CT_coerce_ID_to_TEXT (CT_ident s)
-     -> (match s with
-       "\n" -> [< 'fNL >]
-     | "Retour chariot pour Show proof" -> [< 'fNL >]
-     |_ -> [< 'sTR s >])
-   | CT_text_formula  f -> [< prterm (Hashtbl.find ct_FORMULA_constr f) >]
-  |  CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove");
-	      CT_text_path (CT_signed_int_list p);
-              CT_coerce_ID_to_TEXT (CT_ident "goal");
-	      g] ->
+     | CT_coerce_ID_to_TEXT (CT_ident s)
+       -> (match s with
+	     | "\n" -> fnl ()
+	     | "Retour chariot pour Show proof" -> fnl ()
+	     |_ -> str s)
+     | CT_text_formula  f -> prterm (Hashtbl.find ct_FORMULA_constr f)
+     | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove");
+		   CT_text_path (CT_signed_int_list p);
+		   CT_coerce_ID_to_TEXT (CT_ident "goal");
+		   g] ->
       let p=(List.map (fun y -> match y with
 	                 (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
-      h 0 [<  'sTR "<b>"; sp_print g; 'sTR "</b>">]
+      h 0 (str "<b>" ++ sp_print g ++ str "</b>")
  |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "uselemma");
               CT_coerce_ID_to_TEXT (CT_ident intro);
 	      l;g] ->
-      h 0 [< 'sTR ("<i>("^intro^" "); sp_print l; 'sTR ")</i>"; sp_print g>]
+      h 0 (str ("<i>("^intro^" ") ++ sp_print l ++ str ")</i>" ++ sp_print g)
  |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "hyp");
 	      CT_text_path (CT_signed_int_list p);
 	      CT_coerce_ID_to_TEXT (CT_ident hyp);
@@ -153,7 +153,7 @@ let rec sp_print x =
 	                  (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
-            h 0 [< 'sTR hyp>]
+            h 0 (str hyp)
 
   |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "hyp_with_type");
 	      CT_text_path (CT_signed_int_list p);
@@ -163,23 +163,23 @@ let rec sp_print x =
                          (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
-      h 0 [< sp_print g; 'sPC; 'sTR "<i>("; 'sTR hyp;'sTR ")</i>">]   
+      h 0 (sp_print g ++ spc () ++ str "<i>(" ++ str hyp ++ str ")</i>")   
 
   | CT_text_h l ->
-      h 0 [< prlist_with_sep (fun () -> [< >])
-		(fun y -> sp_print y) l>]
+      h 0 (prlist_with_sep (fun () -> mt ())
+	     (fun y -> sp_print y) l)
   | CT_text_v l ->
-      v 0 [< prlist_with_sep (fun () -> [< >])
-		(fun y -> sp_print y) l>]
+      v 0 (prlist_with_sep (fun () -> mt ())
+		(fun y -> sp_print y) l)
   | CT_text_hv l ->
-      h 0 [< prlist_with_sep (fun () -> [<>])
-		(fun y -> sp_print y) l>]
+      h 0 (prlist_with_sep (fun () -> mt ())
+	     (fun y -> sp_print y) l)
   | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "shrink");
 	      CT_text_op [CT_coerce_ID_to_TEXT (CT_ident info); t]]  ->
-                   h 0 [< 'sTR ("("^info^": "); sp_print t ;'sTR ")" >]
+                   h 0 (str ("("^info^": ") ++ sp_print t ++ str ")")
   | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "root_of_text_proof");
               t]->
                     sp_print t 
-  | _ -> [< 'sTR "..." >]
+  | _ -> str "..."
 ;;
   
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index 75cd7db387..c691ff912e 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -56,12 +56,12 @@ let dbize_sp =
       | Invalid_argument _ | Failure _ ->
       anomaly_loc
        (loc, "Translate.dbize_sp (taken from Astterm)",
-       [< 'sTR "malformed section-path" >])
+       [< str "malformed section-path" >])
     end
     | ast ->
      anomaly_loc
       (Ast.loc ast, "Translate.dbize_sp (taken from Astterm)",
-      [< 'sTR "not a section-path" >]);;
+      [< str "not a section-path" >]);;
 *)
 
 (* dead code:
@@ -120,8 +120,9 @@ let translate_sign env =
     fold_named_context
       (fun env (id,v,c) l -> 
 	 (CT_premise(CT_ident(string_of_id id), translate_constr env c))::l)
-      env [] in
-    CT_premises_list l;;
+      env ~init:[] 
+  in
+  CT_premises_list l;;
        
 (* the function rev_and_compact performs two operations:
    1- it reverses the list of integers given as argument
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 8e1d904894..729b3278d9 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -86,7 +86,7 @@ let make_clenv_binding_apply wc (c,t) lbind =
     clenv_match_args lbind clause
   else 
     errorlabstrm "make_clenv_bindings"
-      [<'sTR "Cannot mix bindings and free associations">]
+      (str "Cannot mix bindings and free associations")
 
 let resolve_with_bindings_tac  (c,lbind) gl = 
   let (wc,kONT) = startWalk gl in
@@ -107,13 +107,13 @@ let reduce_to_mind gl t =
 	   let t' = pf_nf_betaiota gl (pf_one_step_reduce gl t) in elimrec t' l
          with e when catchable_exception e -> 
 	   errorlabstrm "tactics__reduce_to_mind"
-             [< 'sTR"Not an inductive product" >])
+             (str"Not an inductive product"))
     | (Case _,_) ->
 	(try 
 	   let t' = pf_nf_betaiota gl (pf_one_step_reduce gl t) in elimrec t' l
          with e when catchable_exception e -> 
 	   errorlabstrm "tactics__reduce_to_mind"
-             [< 'sTR"Not an inductive product" >])
+             (str"Not an inductive product"))
     | (Cast (c,_),[]) -> elimrec c l
     | (Prod (n,ty,t'),[]) -> 
 	let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in
@@ -487,7 +487,7 @@ let context operation path (t : constr) =
       | ((P_TYPE :: p), LetIn (n,b,t,c)) ->
 	  (mkLetIn (n,b,loop i p t,c))
       | (p, _) -> 
-	  pPNL [<Printer.prterm t>];
+	  ppnl (Printer.prterm t);
 	  failwith ("abstract_path " ^ string_of_int(List.length p)) 
   in
   loop 1 path t
@@ -508,7 +508,7 @@ let occurence path (t : constr) =
     | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
     | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
     | (p, _) -> 
-	pPNL [<Printer.prterm t>];
+	ppnl (Printer.prterm t);
 	failwith ("occurence " ^ string_of_int(List.length p)) 
   in
   loop path t
@@ -1658,8 +1658,8 @@ let rec decidability gl t =
           | Kapp("Z",[]) ->  mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
           | Kapp("nat",[]) ->  mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
           | _ -> errorlabstrm "decidability" 
-		[< 'sTR "Omega: Can't solve a goal with equality on "; 
-		   Printer.prterm typ >]
+		(str "Omega: Can't solve a goal with equality on " ++ 
+		   Printer.prterm typ)
 	end
     | Kapp("Zne",[t1;t2]) -> mkApp (Lazy.force coq_dec_Zne, [| t1;t2 |])
     | Kapp("Zle",[t1;t2]) -> mkApp (Lazy.force coq_dec_Zle, [| t1;t2 |])
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 97258c5063..83ed2ad141 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -215,9 +215,9 @@ let guess_theory a =
     theories_map_find a
   with Not_found -> 
     errorlabstrm "Ring" 
-      [< 'sTR "No Declared Ring Theory for ";
-	 prterm a; 'fNL;
-	 'sTR "Use Add [Semi] Ring to declare it">]
+      (str "No Declared Ring Theory for " ++
+	 prterm a ++ fnl () ++
+	 str "Use Add [Semi] Ring to declare it")
 
 (* Looks up an option *)
 
@@ -229,8 +229,8 @@ let unbox = function
 
 let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset = 
   if theories_map_mem a then errorlabstrm "Add Semi Ring" 
-    [< 'sTR "A (Semi-)(Setoid-)Ring Structure is already declared for ";
-       prterm a >];
+    (str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++
+       prterm a);
   let env = Global.env () in
     if (want_ring & want_setoid &
 	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
@@ -238,24 +238,24 @@ let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus
 			[| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])))) &
 	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth))
 		(mkLApp (coq_Setoid_Theory, [| a; (unbox aequiv) |]))))) then 
-      errorlabstrm "addring" [< 'sTR "Not a valid Setoid-Ring theory" >];
+      errorlabstrm "addring" (str "Not a valid Setoid-Ring theory");
     if (not want_ring & want_setoid &
 	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
 		(mkLApp (coq_Semi_Setoid_Ring_Theory, 
 			[| a; (unbox aequiv); aplus; amult; aone; azero; aeq|])))) &
 	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth))
 		(mkLApp (coq_Setoid_Theory, [| a; (unbox aequiv) |]))))) then 
-      errorlabstrm "addring" [< 'sTR "Not a valid Semi-Setoid-Ring theory" >];
+      errorlabstrm "addring" (str "Not a valid Semi-Setoid-Ring theory");
     if (want_ring & not want_setoid &
 	not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
 	       (mkLApp (coq_Ring_Theory, 
 		       [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])))) then
-      errorlabstrm "addring" [< 'sTR "Not a valid Ring theory" >];
+      errorlabstrm "addring" (str "Not a valid Ring theory");
     if (not want_ring & not want_setoid &
 	not (is_conv  env Evd.empty (Typing.type_of env Evd.empty t) 
 	       (mkLApp (coq_Semi_Ring_Theory, 
 		       [| a; aplus; amult; aone; azero; aeq |])))) then 
-      errorlabstrm "addring" [< 'sTR "Not a valid Semi-Ring theory" >];
+      errorlabstrm "addring" (str "Not a valid Semi-Ring theory");
     Lib.add_anonymous_leaf
       (theory_to_obj 
 	 (a, { th_ring = want_ring;
@@ -931,7 +931,7 @@ let polynom lc gl =
 		 (fun c1 -> not (pf_conv_x gl t (pf_type_of gl c1))) args
 	       then 
 		 errorlabstrm "Ring :"
-		   [< 'sTR" All terms must have the same type" >];
+		   (str" All terms must have the same type");
 	       (tclTHEN (raw_polynom th None args) (guess_eq_tac th)) gl
 	   | _ -> (match match_with_equiv (pf_concl gl) with
 		     | Some (equiv, c1::args) ->
@@ -941,10 +941,10 @@ let polynom lc gl =
 			     (fun c2 -> not (pf_conv_x gl t (pf_type_of gl c2))) args
 			   then 
 			     errorlabstrm "Ring :"
-			       [< 'sTR" All terms must have the same type" >];
+			       (str" All terms must have the same type");
 			   (tclTHEN (raw_polynom th None args) (guess_equiv_tac th)) gl		   
 		     | _ -> errorlabstrm "polynom :" 
-			 [< 'sTR" This goal is not an equality nor a setoid equivalence" >]))
+			 (str" This goal is not an equality nor a setoid equivalence")))
     (* Elsewhere, guess the theory, check that all terms have the same type
        and apply raw_polynom *)
     | c :: lc' -> 
@@ -954,7 +954,7 @@ let polynom lc gl =
 	    (fun c1 -> not (pf_conv_x gl t (pf_type_of gl c1))) lc'
 	  then 
 	    errorlabstrm "Ring :"
-	      [< 'sTR" All terms must have the same type" >];
+	      (str" All terms must have the same type");
 	  (tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl
 
 let dyn_polynom ltacargs gl =  
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index 791a2fafa0..0ec6926336 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -513,7 +513,7 @@ let replay_history env_hyp =
   in loop env_hyp
 
 let show_goal gl =
-  if !debug then Pp.pPNL (Tacmach.pr_gls gl); Tacticals.tclIDTAC gl
+  if !debug then Pp.ppnl (Tacmach.pr_gls gl); Tacticals.tclIDTAC gl
 
 (* Cette fonction prépare le rejeu puis l'appelle :
    \begin{itemize}
@@ -569,9 +569,9 @@ let prepare_and_play env tac_hyps trace_solution =
     mkApp(Lazy.force coq_interp_sequent, [| env_reified; l_reified_terms |]) in
   let reified_trace_solution = replay_history l_e trace_solution in
   if !debug then begin
-    Pp.pPNL [< Printer.prterm reified>];
-    Pp.pPNL [< Printer.prterm l_reified_tac_norms>];
-    Pp.pPNL [< Printer.prterm reified_trace_solution>];
+    Pp.ppnl (Printer.prterm reified);
+    Pp.ppnl (Printer.prterm l_reified_tac_norms);
+    Pp.ppnl (Printer.prterm reified_trace_solution);
   end;
   Tactics.generalize l_generalized >>
   Tactics.change_in_concl reified >>