compat ocaml 3.03

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

18 files changed, 350 insertions, 343 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
index 1830e45e9f..ac5c149e4a 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -37,7 +37,7 @@ let slam(idl,b) = Slam(dummy_loc,idl,b)
 let ide s = Id(dummy_loc,s)
 let nvar s = Nvar(dummy_loc,s)
 let num n = Num(dummy_loc,n)
-let str s = Str(dummy_loc,s)
+let string s = Str(dummy_loc,s)
 let path sl = Path(dummy_loc,sl)
 let dynamic d = Dynamic(dummy_loc,d)
 
@@ -102,63 +102,67 @@ type env = (string * v) list
 (* Pretty-printing *)
 let rec print_ast ast =
   match ast with
-    | Num(_,n) -> [< 'iNT n >]
-    | Str(_,s) -> [< 'qS s >]
-    | Path(_,sl) -> [< 'sTR(string_of_path sl) >]
-    | Id (_,s) -> [< 'sTR"{" ; 'sTR s ; 'sTR"}" >]
-    | Nvar(_,s) -> [< 'sTR(string_of_id s) >]
-    | Nmeta(_,s) -> [< 'sTR s >]
+    | Num(_,n) -> int n
+    | Str(_,s) -> qs s
+    | Path(_,sl) -> str (string_of_path sl)
+    | Id (_,s) -> str "{" ++ str s ++ str "}"
+    | Nvar(_,s) -> str (string_of_id s)
+    | Nmeta(_,s) -> str s
     | Node(_,op,l) ->
-        hOV 3 [< 'sTR"(" ; 'sTR op ; 'sPC ; print_astl l; 'sTR")" >]
-    | Slam(_,None,ast) -> hOV 1 [< 'sTR"[<>]"; print_ast ast >]
+        hov 3 (str "(" ++ str op ++ spc () ++ print_astl l ++ str ")")
+    | Slam(_,None,ast) -> hov 1 (str "[<>]" ++ print_ast ast)
     | Slam(_,Some x,ast) ->
-        hOV 1
-          [< 'sTR"["; 'sTR(string_of_id x); 'sTR"]"; 'cUT; print_ast ast >]
-    | Smetalam(_,id,ast) -> hOV 1 [< 'sTR id; print_ast ast >]
+        hov 1
+          (str "[" ++ str (string_of_id x) ++ str "]" ++ cut () ++ 
+	   print_ast ast)
+    | Smetalam(_,id,ast) -> hov 1 (str id ++ print_ast ast)
     | Dynamic(_,d) ->
-	hOV 0 [< 'sTR"<dynamic: "; 'sTR(Dyn.tag d); 'sTR">" >]
+	hov 0 (str "<dynamic: " ++ str (Dyn.tag d) ++ str ">")
 
 and print_astl astl =
   prlist_with_sep pr_spc print_ast astl
 
 let print_ast_cast = function
-  | Tany -> [< >]
-  | Tvar -> [< 'sTR":var" >]
-  | Tid -> [< 'sTR":id" >]
-  | Tstr -> [< 'sTR":str" >]
-  | Tpath -> [< 'sTR":path" >]
-  | Tnum -> [< 'sTR":num" >]
-  | Tlist -> [< 'sTR":list" >]
+  | Tany -> (mt ())
+  | Tvar -> (str":var")
+  | Tid -> (str":id")
+  | Tstr -> (str":str")
+  | Tpath -> (str":path")
+  | Tnum -> (str":num")
+  | Tlist -> (str":list")
 
 let rec print_astpat = function
-  | Pquote ast -> [< 'sTR"'"; print_ast ast >]
-  | Pmeta(s,tk) -> [< 'sTR s; print_ast_cast tk >]
+  | Pquote ast -> 
+      str"'" ++ print_ast ast 
+  | Pmeta(s,tk) -> 
+      str s ++ print_ast_cast tk 
   | Pmeta_slam(s,b) ->
-      hOV 1 [< 'sTR"["; 'sTR s; 'sTR"]"; 'cUT; print_astpat b >]
+      hov 1 (str "[" ++ str s ++ str"]" ++ cut () ++ print_astpat b)
   | Pnode(op,al) ->
-      hOV 2 [< 'sTR"(" ; 'sTR op; 'sPC; print_astlpat al; 'sTR")" >]
-  | Pslam(None,b) -> hOV 1 [< 'sTR"[<>]"; 'cUT; print_astpat b >]
+      hov 2 (str"("  ++ str op ++ spc () ++ print_astlpat al ++ str")" )
+  | Pslam(None,b) -> 
+      hov 1 (str"[<" ++ cut () ++ print_astpat b)
   | Pslam(Some id,b) ->
-      hOV 1
-        [< 'sTR"["; 'sTR(string_of_id id); 'sTR"]"; 'cUT; print_astpat b >]
+      hov 1
+        (str"[" ++ str(string_of_id id) ++ str"]" ++ cut () ++ print_astpat b)
 
 and print_astlpat = function
-  | Pnil -> [< >]
-  | Pcons(h,Pnil) -> hOV 1 [< print_astpat h >]
-  | Pcons(h,t) -> hOV 1 [< print_astpat h; 'sPC; print_astlpat t >]
-  | Plmeta(s) -> [< 'sTR"| "; 'sTR s >]
+  | Pnil -> (mt ())
+  | Pcons(h,Pnil) -> hov 1 (print_astpat h)
+  | Pcons(h,t) -> hov 1 (print_astpat h ++ spc () ++ print_astlpat t)
+  | Plmeta(s) -> (str"| " ++ str s)
 
 
 let print_val = function
   | Vast a -> print_ast a
   | Vastlist al -> 
-      hOV 1 [< 'sTR"["; prlist_with_sep pr_spc print_ast al; 'sTR"]" >]
+      hov 1 (str"[" ++ prlist_with_sep pr_spc print_ast al ++ str"]")
 
 
 (* Ast values environments *)
 
 let grammar_type_error (loc,s) =
-  anomaly_loc (loc,s,[< 'sTR"grammar type error: "; 'sTR s >])
+  anomaly_loc (loc,s,(str"grammar type error: " ++ str s))
 
 
 (* Coercions enforced by the user *)
@@ -172,7 +176,7 @@ let check_cast loc a k =
     | (Tnum, Num _) -> ()
     | (Tlist, _) -> grammar_type_error (loc,"Ast.cast_val")
     | _ -> user_err_loc (loc,"Ast.cast_val",
-                         [< 'sTR"cast _"; print_ast_cast k; 'sTR"failed" >])
+                         (str"cast _" ++ print_ast_cast k ++ str"failed"))
 
 let rec coerce_to_var = function
   | Nvar(_,id) as var -> var
@@ -181,7 +185,7 @@ let rec coerce_to_var = function
   | Node(_,"QUALIDARG",[Nvar(_,id) as var]) -> var
   | ast -> user_err_loc
         (loc ast,"Ast.coerce_to_var",
-         [< 'sTR"This expression should be a simple identifier" >])
+         (str"This expression should be a simple identifier"))
 
 let coerce_to_id a = match coerce_to_var a with
   | Nvar (_,id) -> id
@@ -194,7 +198,7 @@ let env_assoc_value loc v env =
   with Not_found -> 
     anomaly_loc
       (loc,"Ast.env_assoc_value",
-       [< 'sTR"metavariable "; 'sTR v; 'sTR" is unbound." >])
+       (str"metavariable " ++ str v ++ str" is unbound."))
 
 let env_assoc_list sigma (loc,v) =
   match env_assoc_value loc v sigma with
@@ -252,12 +256,12 @@ let type_of_meta env loc pv =
     List.assoc pv env
   with Not_found ->
     user_err_loc (loc,"Ast.type_of_meta",
-                  [< 'sTR"variable "; 'sTR pv; 'sTR" is unbound" >])
+                  (str"variable " ++ str pv ++ str" is unbound"))
 
 let check_ast_meta env loc pv =
   if (type_of_meta env loc pv) <> ETast then
     user_err_loc (loc,"Ast.check_ast_meta",
-                  [< 'sTR"variable "; 'sTR pv; 'sTR" is a List" >])
+                  (str"variable " ++ str pv ++ str" is a List"))
 
 let rec val_of_ast env ast =
   match ast with
@@ -277,7 +281,7 @@ let rec val_of_ast env ast =
     | Slam(_,os,b) -> Pslam(os, val_of_ast env b)
     | Node(loc,op,_) when isMeta op ->
         user_err_loc(loc,"Ast.val_of_ast",
-                     [< 'sTR"no metavariable in operator position." >])
+                     (str"no metavariable in operator position."))
     | Node(_,op,args) -> Pnode(op, vall_of_astl env args)
     | Dynamic(loc,_) ->
 	invalid_arg_loc(loc,"val_of_ast: dynamic")
@@ -292,8 +296,8 @@ and vall_of_astl env astl =
 	    Pcons(Pmeta(pv,Tlist), vall_of_astl env asttl)
         else 
 	  user_err_loc (loc,"Ast.vall_of_astl",
-                        [< 'sTR"variable "; 'sTR pv;
-                           'sTR" is not a List" >])
+                        (str"variable " ++ str pv ++
+                           str" is not a List"))
     | ast::asttl -> 
 	Pcons (val_of_ast env ast, vall_of_astl env asttl)
     | [] -> Pnil
@@ -449,8 +453,8 @@ let bind_patvar env loc v etyp =
     else 
       user_err_loc
 	(loc,"Ast.bind_patvar",
-	 [< 'sTR"variable "; 'sTR v;
-            'sTR" is bound several times with different types" >])
+	 (str"variable " ++ str v ++
+            str" is bound several times with different types"))
   with Not_found -> 
     if v="$_" then env else (v,etyp)::env
       
@@ -493,7 +497,7 @@ let rec pat_of_ast env ast =
         (Pslam(os,pb), env')
     | Node(loc,op,_) when isMeta op ->
         user_err_loc(loc,"Ast.pat_of_ast",
-                     [< 'sTR"no metavariable in operator position." >])
+                     (str"no metavariable in operator position."))
     | Node(_,op,args) ->
         let (pargs, env') = patl_of_astl env args in
         (Pnode(op,pargs), env')
@@ -521,28 +525,29 @@ let to_pat env ast =
 (* Ast with cases and metavariables *)
 
 let print_sig = function
-  | [] -> [< >]
+  | [] -> 
+      mt ()
   | sigma ->
-      [< 'sTR"with constraints :"; 'bRK(1,1);
-         v 0 (prlist_with_sep pr_spc
-                (fun (x,v) -> [< 'sTR x; 'sTR" = "; hOV 0 (print_val v) >])
-                sigma) >]
+      str"with constraints :" ++ brk(1,1) ++
+      v 0 (prlist_with_sep pr_spc
+             (fun (x,v) -> str x ++ str" = " ++ hov 0 (print_val v))
+             sigma)
 
 let case_failed loc sigma e pats =
   user_err_loc
     (loc,"Ast.eval_act",
-     [< 'sTR"Grammar case failure. The ast"; 'sPC; print_ast e;
-        'sPC; 'sTR"does not match any of the patterns :";
-        'bRK(1,1); v 0 (prlist_with_sep pr_spc print_astpat pats); 'fNL;
-        print_sig sigma >])
+     str"Grammar case failure. The ast" ++ spc () ++ print_ast e ++
+     spc () ++ str"does not match any of the patterns :" ++
+     brk(1,1) ++ v 0 (prlist_with_sep pr_spc print_astpat pats) ++ fnl () ++
+     print_sig sigma)
 
 let caselist_failed loc sigma el pats =
   user_err_loc
     (loc,"Ast.eval_act",
-     [< 'sTR"Grammar case failure. The ast list"; 'bRK(1,1); print_astl el;
-        'sPC; 'sTR"does not match any of the patterns :";
-        'bRK(1,1); v 0 (prlist_with_sep pr_spc print_astlpat pats); 'fNL;
-        print_sig sigma >])
+     str"Grammar case failure. The ast list" ++ brk(1,1) ++ print_astl el ++
+     spc () ++ str"does not match any of the patterns :" ++
+     brk(1,1) ++ v 0 (prlist_with_sep pr_spc print_astlpat pats) ++ fnl () ++
+     print_sig sigma)
 
 let rec eval_act dloc sigma act =
   match act with
@@ -593,7 +598,7 @@ and case vars etyp ast =
                (apl,aa)
            | _ -> user_err_loc
                  (loca,"Ast.case",
-                  [< 'sTR"case pattern for an ast should be a single ast" >]))
+                  (str"case pattern for an ast should be a single ast")))
     | _ -> invalid_arg_loc (loc ast,"Ast.case")
 	  
 and caselist vars etyp ast =
diff --git a/parsing/ast.mli b/parsing/ast.mli
index d3e0ee4ab2..fae49ac34c 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -25,7 +25,7 @@ val slam : identifier option * Coqast.t -> Coqast.t
 val nvar : identifier -> Coqast.t
 val ide : string -> Coqast.t
 val num : int -> Coqast.t
-val str : string -> Coqast.t
+val string : string -> Coqast.t
 val path : section_path -> Coqast.t
 val dynamic : Dyn.t -> Coqast.t
 
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index b471059f4a..e2baa7b77c 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -34,28 +34,28 @@ let from_list l = List.fold_right Idset.add l Idset.empty
 
 (* when an head ident is not a constructor in pattern *)
 let mssg_hd_is_not_constructor s =
-  [< 'sTR "The symbol "; pr_id s; 'sTR " should be a constructor" >]
+  (str "The symbol " ++ pr_id s ++ str " should be a constructor")
 
 (* checking linearity of a list of ids in patterns *)
 let non_linearl_mssg id =
-  [< 'sTR "The variable " ; 'sTR(string_of_id id);
-     'sTR " is bound several times in pattern" >] 
+  (str "The variable " ++ str(string_of_id id) ++
+     str " is bound several times in pattern") 
 
 let error_capture_loc loc s =
   user_err_loc
     (loc,"ast_to_rawconstr", 
-     [< 'sTR "The variable "; pr_id s; 'sTR " occurs in its type" >])
+     (str "The variable " ++ pr_id s ++ str " occurs in its type"))
 
 let error_expl_impl_loc loc =
   user_err_loc
     (loc,"ast_to_rawconstr", 
-     [< 'sTR "Found an explicitely given implicit argument but was expecting";
-	'fNL; 'sTR "a regular one" >])
+     (str "Found an explicitely given implicit argument but was expecting" ++
+	fnl () ++ str "a regular one"))
 
 let error_metavar_loc loc =
   user_err_loc
     (loc,"ast_to_rawconstr", 
-     [< 'sTR "Metavariable numbers must be positive" >])
+     (str "Metavariable numbers must be positive"))
 
 let rec has_duplicate = function 
   | [] -> None
@@ -70,17 +70,17 @@ let check_linearity lhs ids =
     | None -> ()
 
 let mal_formed_mssg () =
-  [<'sTR "malformed macro of multiple case" >]
+  (str "malformed macro of multiple case")
 
 (* determines if some pattern variable starts with uppercase *)
 let warning_uppercase loc uplid = (* Comment afficher loc ?? *)
   let vars =
     prlist_with_sep 
-      (fun () -> [< 'sTR ", " >]) (* We avoid 'sPC, else it breaks the line *)
-      (fun v -> [< 'sTR (string_of_id v) >]) uplid in
+      (fun () -> (str ", ")) (* We avoid spc (), else it breaks the line *)
+      (fun v -> (str (string_of_id v))) uplid in
   let (s1,s2) = if List.length uplid = 1 then (" ","s ") else ("s "," ") in
-  wARN [<'sTR ("the variable"^s1); vars;
-	 'sTR (" start"^s2^"with an upper case letter in pattern") >]
+  warn (str ("the variable"^s1) ++ vars ++
+	str (" start"^s2^"with an upper case letter in pattern"))
 
 let is_uppercase_var v =
  match (string_of_id v).[0] with
@@ -96,8 +96,8 @@ let check_uppercase loc ids =
 
 (* check that the number of pattern matches the number of matched args *)
 let mssg_number_of_patterns n pl =
-  [< 'sTR"Expecting ";'iNT n ; 'sTR" pattern(s) but found ";
-    'iNT (List.length pl); 'sTR" in " >]
+  str"Expecting " ++ int n  ++ str" pattern(s) but found " ++
+  int (List.length pl) ++ str" in "
 
 let check_number_of_pattern loc n l =
   if n<>(List.length l) then
@@ -115,9 +115,9 @@ let ast_to_sp = function
 	 section_path sp
        with Invalid_argument _ | Failure _ ->
          anomaly_loc(loc,"Astterm.ast_to_sp",
-                     [< 'sTR"ill-formed section-path" >]))
+                     (str"ill-formed section-path")))
   | ast -> anomaly_loc(Ast.loc ast,"Astterm.ast_to_sp",
-                     [< 'sTR"not a section-path" >])
+                     (str"not a section-path"))
 
 let is_underscore id = (id = wildcard)
 
@@ -126,7 +126,7 @@ let name_of_nvar s =
 
 let ident_of_nvar loc s =
   if is_underscore s then
-    user_err_loc (loc,"ident_of_nvar", [< 'sTR "Unexpected wildcard" >])
+    user_err_loc (loc,"ident_of_nvar", (str "Unexpected wildcard"))
   else s
 
 let interp_qualid p =
@@ -190,8 +190,8 @@ let maybe_constructor env = function
 
   | Node(loc,("CONST"|"EVAR"|"MUTIND"|"SYNCONST" as key), l) ->
       user_err_loc (loc,"ast_to_pattern",
-   [< 'sTR "Found a pattern involving global references which are not constructors"
-   >])
+   (str "Found a pattern involving global references which are not constructors"
+))
 
   | _ -> anomaly "ast_to_pattern: badly-formed ast for Cases pattern"
 
@@ -214,7 +214,7 @@ let ast_to_global loc c =
     | ("SYNCONST", [sp]) ->
 	Syntax_def.search_syntactic_definition (ast_to_sp sp), []
     | _ -> anomaly_loc (loc,"ast_to_global",
-			[< 'sTR "Bad ast for this global a reference">])
+			(str "Bad ast for this global a reference"))
 
 (*
 let ref_from_constr c = match kind_of_term c with
@@ -338,12 +338,12 @@ let rec ast_to_cofix = function
       (fi::lf, astA::lA, astT::lt)
   | _ -> anomaly "CFDECL is expected"
 
-let error_fixname_unbound str is_cofix loc name = 
+let error_fixname_unbound s is_cofix loc name = 
   user_err_loc 
     (loc,"ast_to (COFIX)",
-       [< 'sTR "The name"; 'sPC ; pr_id name ; 
-	  'sPC ; 'sTR "is not bound in the corresponding"; 'sPC ;
-	  'sTR ((if is_cofix then "co" else "")^"fixpoint definition") >])
+     str "The name" ++ spc () ++ pr_id name ++ 
+     spc () ++ str "is not bound in the corresponding" ++ spc () ++
+     str ((if is_cofix then "co" else "")^"fixpoint definition"))
 (*
 let rec collapse_env n env = if n=0 then env else
   add_rel_decl (Anonymous,()) (collapse_env (n-1) (snd (uncons_rel_env env)))
@@ -458,7 +458,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 
     | Node(loc,"SQUASH",_) ->
         user_err_loc(loc,"ast_to_rawconstr",
-                     [< 'sTR "Ill-formed specification" >])
+                     (str "Ill-formed specification"))
 
     | Node(loc,opn,tl) -> 
 	anomaly ("ast_to_rawconstr found operator "^opn^" with "^
@@ -664,10 +664,10 @@ let constrOut = function
     if (Dyn.tag d) = "constr" then
       constr_out d
     else
-      anomalylabstrm "constrOut" [<'sTR "Dynamic tag should be constr">]
+      anomalylabstrm "constrOut" (str "Dynamic tag should be constr")
   | ast ->
     anomalylabstrm "constrOut"
-      [<'sTR "Not a Dynamic ast: "; print_ast ast>]
+      (str "Not a Dynamic ast: " ++ print_ast ast)
 
 let interp_constr sigma env c =
   understand sigma env (interp_rawconstr sigma env c)
@@ -688,13 +688,13 @@ let interp_sort = function
   | Node(loc,"PROP", []) -> Prop Null
   | Node(loc,"SET", [])  -> Prop Pos
   | Node(loc,"TYPE", _) -> new_Type_sort ()
-  | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
+  | a -> user_err_loc (Ast.loc a,"interp_sort", (str "Not a sort"))
 
 let interp_elimination_sort = function
   | Node(loc,"PROP", []) -> InProp
   | Node(loc,"SET", [])  -> InSet
   | Node(loc,"TYPE", _) -> InType
-  | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
+  | a -> user_err_loc (Ast.loc a,"interp_sort", (str "Not a sort"))
 
 let judgment_of_rawconstr sigma env c =
   understand_judgment sigma env (interp_rawconstr sigma env c)
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index aa9ab17aa2..fb3039c0ea 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -25,11 +25,11 @@ let (grammar_state : grammar_command list ref) = ref []
 let specify_name name e =
   match e with
     | UserError(lab,strm) ->
-        UserError(lab, [< 'sTR"during interpretation of grammar rule ";
-                          'sTR name; 'sTR","; 'sPC; strm >])
+        UserError(lab, (str"during interpretation of grammar rule " ++
+                          str name ++ str"," ++ spc () ++ strm))
     | Anomaly(lab,strm) ->
-        Anomaly(lab, [< 'sTR"during interpretation of grammar rule ";
-                        'sTR name; 'sTR","; 'sPC; strm >])
+        Anomaly(lab, (str"during interpretation of grammar rule " ++
+                        str name ++ str"," ++ spc () ++ strm))
     | Failure s ->
         Failure("during interpretation of grammar rule "^name^", "^s)
     | e -> e
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index 28be507232..2b801d03eb 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -141,7 +141,7 @@ let _ = Ppprim.add ("token",token_printer)
 
 (* A primitive printer to do "print as" (to specify a length for a string) *)
 let print_as_printer stdpr = function
-  | Node (_, "AS", [Num(_,n); Str(_,s)]) -> [< 'sTRas (n,s) >]
+  | Node (_, "AS", [Num(_,n); Str(_,s)]) -> (stras (n,s))
   | ast                                  -> stdpr ast
 
 let _ = Ppprim.add ("print_as",print_as_printer)
@@ -165,11 +165,11 @@ let print_syntax_entry whatfor sub_pr env se =
             | None -> token_printer (sub_pr whatfor (Some(rule_prec,reln)))
         in 
 	printer (Ast.pat_sub Ast.dummy_loc env e)
-    | RO s -> [< 'sTR s >]
-    | UNP_TAB -> [< 'tAB >]
-    | UNP_FNL -> [< 'fNL >]
-    | UNP_BRK(n1,n2) -> [< 'bRK(n1,n2) >]
-    | UNP_TBRK(n1,n2) -> [< 'tBRK(n1,n2) >]
+    | RO s -> str s
+    | UNP_TAB -> tab ()
+    | UNP_FNL -> fnl ()
+    | UNP_BRK(n1,n2) -> brk(n1,n2)
+    | UNP_TBRK(n1,n2) -> tbrk(n1,n2)
     | UNP_BOX (b,sub) -> ppcmd_of_box b (prlist print_hunk sub)
   in 
   prlist print_hunk se.syn_hunks
@@ -191,11 +191,11 @@ let genprint dflt whatfor inhprec ast =
 	  if no_paren then 
 	    printed_gt
 	  else 
-	    [< 'sTR"(" ; printed_gt; 'sTR")" >]
+	    (str"(" ++ printed_gt ++ str")")
       | None -> dflt gt (* No rule found *)
   in
   try 
     rec_pr whatfor inhprec ast
   with
-    | Failure _ -> [< 'sTR"<PP failure: "; dflt ast; 'sTR">" >]
-    | Not_found -> [< 'sTR"<PP search failure: "; dflt ast; 'sTR">" >]
+    | Failure _ -> (str"<PP failure: " ++ dflt ast ++ str">")
+    | Not_found -> (str"<PP search failure: " ++ dflt ast ++ str">")
diff --git a/parsing/extend.ml4 b/parsing/extend.ml4
index 2c74daa860..e54ac11bba 100644
--- a/parsing/extend.ml4
+++ b/parsing/extend.ml4
@@ -107,7 +107,7 @@ let nterm univ ast =
     try 
       get_entry u n
     with UserError _ -> 
-      user_err_loc(loc ast,"Externd.nterm", [< 'sTR"unknown grammar entry" >])
+      user_err_loc(loc ast,"Externd.nterm", str"unknown grammar entry")
   in
   (nont, type_of_entry e)
 
@@ -163,7 +163,7 @@ let gram_define_entry univ = function
         try 
 	  create_entry univ nt etyp
         with Failure s ->
-          user_err_loc (ntl,"gram_define_entry",[< 'sTR s >])
+          user_err_loc (ntl,"gram_define_entry", str s)
       in 
       (nt, etyp, assoc, rl)
   | ast -> invalid_arg_loc (Ast.loc ast, "gram_define_entry")
@@ -218,8 +218,8 @@ type unparsing_hunk =
 
 let ppcmd_of_box = function
   | PpHB n -> h n
-  | PpHOVB n -> hOV n
-  | PpHVB n -> hV n
+  | PpHOVB n -> hov n
+  | PpHVB n -> hv n
   | PpVB n -> v n
   | PpTB   -> t
 
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index dc69dca1ad..9c008d34df 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -31,14 +31,14 @@ GEXTEND Gram
         (match c with
         | Coqast.Node(_,"COMMAND",[csr]) ->
           <:ast< (LETTOPCLAUSE $id (CONSTR $csr)) >>
-	| _ -> errorlabstrm "Gram.let_clause" [<'sTR "Not a COMMAND">])
+	| _ -> errorlabstrm "Gram.let_clause" (str "Not a COMMAND"))
       | id = identarg; ":"; c = constrarg; ":="; te = tactic_expr ->
         <:ast< (LETCUTCLAUSE $id $c $te) >> 
       |	id = identarg; ":"; c = constrarg ->
         (match c with
         | Coqast.Node(_,"COMMAND",[csr]) ->
           <:ast< (LETTOPCLAUSE $id (CONSTR $csr)) >>
-	| _ -> errorlabstrm "Gram.let_clause" [<'sTR "Not a COMMAND">]) ] ]
+	| _ -> errorlabstrm "Gram.let_clause" (str "Not a COMMAND")) ] ]
   ;
   rec_clause:
     [ [ name = identarg; it = LIST1 input_fun; "->"; body = tactic_atom ->
@@ -51,7 +51,7 @@ GEXTEND Gram
             [Coqast.Node(_,"QUALID",[Coqast.Nvar(_,_) as s])]) ->
           <:ast< (SUBTERM $s $pc) >>
         | _ ->
-          errorlabstrm "Gram.match_pattern" [<'sTR "Not a correct SUBTERM">])
+          errorlabstrm "Gram.match_pattern" (str "Not a correct SUBTERM"))
       | "["; pc = constrarg; "]" -> <:ast< (SUBTERM $pc) >>
       | pc = constrarg -> <:ast< (TERM $pc) >> ] ]
   ;
@@ -117,7 +117,7 @@ GEXTEND Gram
         (match llc with
 	| [Coqast.Node(_,"LETTOPCLAUSE",[id;c])] ->
           <:ast< (TheoremProof "LETTOP" $id $c $tb) >>
-	| _ -> errorlabstrm "Gram.tactic_atom" [<'sTR "Not a LETTOPCLAUSE">])
+	| _ -> errorlabstrm "Gram.tactic_atom" (str "Not a LETTOPCLAUSE"))
       |	IDENT "Match"; IDENT "Context"; IDENT "With"; mrl = match_context_list
         -> <:ast< (MATCHCONTEXT ($LIST $mrl)) >>
       |	IDENT "Match"; com = constrarg; IDENT "With"; mrl = match_list ->
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index 9faf6d877e..8c5df17a7a 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -125,11 +125,11 @@ let print_univers = ref false
 let print_casts = ref false
 
 let print_type u =
-  if !print_univers then [< 'sTR "Type"; pr_uni u >]
-  else [< 'sTR "Type" >]
+  if !print_univers then (str "Type" ++ pr_uni u)
+  else (str "Type")
 
 let print_name = function
-  | Anonymous -> [< 'sTR "_" >]
+  | Anonymous -> (str "_")
   | Name id -> pr_id id
 
 let print_rel bv n = print_name (List.nth bv (pred n))
@@ -145,33 +145,33 @@ let rename bv = function
 
 let rec pp bv t =
   match kind_of_term t with
-  | Sort (Prop Pos) -> [< 'sTR "Set" >]
-  | Sort (Prop Null) -> [< 'sTR "Prop" >]
+  | Sort (Prop Pos) -> (str "Set")
+  | Sort (Prop Null) -> (str "Prop")
   | Sort (Type u) -> print_type u
   | Lambda (na, t, c) ->
-      [< 'sTR"["; print_name na; 'sTR":"; pp bv t; 'sTR"]"; pp (na::bv) c >]
+      (str"[" ++ print_name na ++ str":" ++ pp bv t ++ str"]" ++ pp (na::bv) c)
   | Prod (Anonymous, t, c) ->
-      [< pp bv t; 'sTR"->"; pp (Anonymous::bv) c >]
+      (pp bv t ++ str"->" ++ pp (Anonymous::bv) c)
   | Prod (na, t, c) ->
-      [< 'sTR"("; print_name na; 'sTR":"; pp bv t; 'sTR")"; pp (na::bv) c >]
+      (str"(" ++ print_name na ++ str":" ++ pp bv t ++ str")" ++ pp (na::bv) c)
   | Cast (c, t) ->
       if !print_casts then 
-	[< 'sTR"("; pp bv c; 'sTR"::"; pp bv t; 'sTR")" >]
+	(str"(" ++ pp bv c ++ str"::" ++ pp bv t ++ str")")
       else 
 	pp bv c
   | App(h, v) ->
-      [< 'sTR"("; pp bv h; 'sPC;
-         prvect_with_sep (fun () -> [< 'sPC >]) (pp bv) v; 'sTR")" >]
+      (str"(" ++ pp bv h ++ spc () ++
+         prvect_with_sep (fun () -> (spc ())) (pp bv) v ++ str")")
   | Const (sp, _) ->
-      [< 'sTR"Const "; pr_id (basename sp) >]
+      (str"Const " ++ pr_id (basename sp))
   | Ind ((sp,i), _) ->
-      [< 'sTR"Ind "; pr_id (basename sp); 'sTR" "; 'iNT i >]
+      (str"Ind " ++ pr_id (basename sp) ++ str" " ++ int i)
   | Construct (((sp,i),j), _) ->
-      [< 'sTR"Construct "; pr_id (basename sp); 'sTR" "; 'iNT i; 
-	 'sTR" "; 'iNT j >]
+      (str"Construct " ++ pr_id (basename sp) ++ str" " ++ int i ++ 
+	 str" " ++ int j)
   | Var id -> pr_id id
   | Rel n -> print_rel bv n
-  | _ -> [< 'sTR"<???>" >]
+  | _ -> (str"<???>")
 
 let pr_term _ ctx = pp (fold_rel_context (fun _ (n,_,_) l -> n::l) ctx [])
 
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 6b67c1c0a4..9a97f4b06d 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -84,7 +84,7 @@ let replace_S p =
 (* Prints not p, but the SUCCESSOR of p !!!!! *)
 let nat_printer std_pr p =
   match (int_of_nat p) with
-    | Some i -> [< 'sTR (string_of_int i) >]
+    | Some i -> (str (string_of_int i))
     | None -> std_pr (replace_S p)
 
 let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer)
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index fdd29feeeb..5e8d853ee0 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -112,7 +112,7 @@ GEXTEND Gram
          | Coqast.Node(_,"RECCLAUSE",nme::[bd]) ->
            <:ast<(TACDEF $nme (AST $bd))>>
          | _ ->
-             anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">])
+             anomalylabstrm "Gram.vernac" (str "Not a correct RECCLAUSE"))
       | IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause; "And";
         vcl=LIST1 vrec_clause SEP "And" ->
         let nvcl=
@@ -123,8 +123,10 @@ GEXTEND Gram
              | Coqast.Node(_,"RECCLAUSE",nme::[bd]) ->
                nme::<:ast<(AST $bd)>>::b
              | _ ->
-               anomalylabstrm "Gram.vernac" [<'sTR
-                 "Not a correct RECCLAUSE">]) (vc::vcl) [] in
+               anomalylabstrm "Gram.vernac" 
+		 (str "Not a correct RECCLAUSE"))
+	    (vc::vcl) []
+	in
         <:ast<(TACDEF ($LIST $nvcl))>>
 
 (* Hints for Auto and EAuto *)
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index ff42bc01d0..41fe0df2ad 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -71,13 +71,13 @@ let replace_plus p =
 let r_printer std_pr p =
  let (_,ast1,astp,_) = get_r_sign dummy_loc in
   match (int_of_r p) with
-    | Some i -> [< 'sTR (string_of_int (i+1)) >]
+    | Some i -> (str (string_of_int (i+1)))
     | None -> std_pr (replace_plus p)
 
 let r_printer_outside std_pr p =
  let (_,ast1,astp,_) = get_r_sign dummy_loc in
   match (int_of_r p) with
-    | Some i -> [< 'sTR "``"; 'sTR (string_of_int (i+1)); 'sTR "``" >]
+    | Some i -> (str "``" ++ str (string_of_int (i+1)) ++ str "``")
     | None -> std_pr (replace_plus p)
 
 let _ = Esyntax.Ppprim.add ("r_printer", r_printer)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5cbfd49542..b58dc654dc 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -369,7 +369,7 @@ GEXTEND Gram
             | (false, _) -> <:ast< (CALL $id ($LIST $l)) >>
             | _ -> Util.user_err_loc
                   (loc, "G_tactic.meta_tactic",
-                   [< 'sTR"Cannot apply arguments to a meta-tactic." >])
+                   (str"Cannot apply arguments to a meta-tactic."))
       ] *)]
   ;
   tactic:
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 8b94b4fd7b..f6a836942e 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -117,9 +117,9 @@ let inside_printer posneg std_pr p =
   match (int_array_option_of_pos astxI astxO astxH p) with
     | Some n -> 
 	if posneg then 
-	  [< 'sTR (string_of_int_array n) >]
+	  (str (string_of_int_array n))
 	else 
-	  [< 'sTR "(-"; 'sTR (string_of_int_array n); 'sTR ")" >]
+	  (str "(-" ++ str (string_of_int_array n) ++ str ")")
     | None -> 
 	let c = if posneg then myvar0 else myvar1 in
 	std_pr (ope("ZEXPR",[ope("APPLIST",[c; p])]))
@@ -129,12 +129,12 @@ let outside_printer posneg std_pr p =
   match (int_array_option_of_pos astxI astxO astxH p) with
     | Some n -> 
 	if posneg then 
-	  [< 'sTR "`"; 'sTR (string_of_int_array n); 'sTR "`">]
+	  (str "`" ++ str (string_of_int_array n) ++ str "`")
 	else 
-	  [< 'sTR "`-"; 'sTR (string_of_int_array n); 'sTR "`" >]
+	  (str "`-" ++ str (string_of_int_array n) ++ str "`")
       | None -> 
 	  let c = if posneg then myvar0 else myvar1 in
-	  [< 'sTR "("; std_pr (ope("APPLIST",[c; p])); 'sTR ")" >] 
+	  (str "(" ++ std_pr (ope("APPLIST", [c; p])) ++ str ")") 
 
 (* Declare pretty-printers for integers *)
 let _ = Esyntax.Ppprim.add ("positive_printer", (outside_printer true))
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 540e1fab01..ffa82f0342 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -73,8 +73,7 @@ module Gram =
       :: !camlp4_state;
       G.extend e pos rls
     let delete_rule e pil =
-      errorlabstrm "Pcoq.delete_rule"
-        [< 'sTR "GDELETE_RULE forbidden." >]
+      errorlabstrm "Pcoq.delete_rule" (str "GDELETE_RULE forbidden.")
   end
 
 
@@ -192,7 +191,7 @@ let get_entry (u, utab) s =
     Hashtbl.find utab s 
   with Not_found -> 
     errorlabstrm "Pcoq.get_entry"
-      [< 'sTR"unknown grammar entry "; 'sTR u; 'sTR":"; 'sTR s >]
+      (str "unknown grammar entry " ++ str u ++ str ":" ++ str s)
       
 let new_entry etyp (u, utab) s =
   let ename = u ^ ":" ^ s in
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 4ee2329156..41a4a6b5a4 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -32,18 +32,18 @@ let print_basename sp = pr_global (ConstRef sp)
 let print_closed_sections = ref false
 
 let print_typed_value_in_env env (trm,typ) =
-  [< prterm_env env trm ; 'fNL ;
-     'sTR "     : "; prtype_env env typ ; 'fNL >]
+  (prterm_env env trm ++ fnl () ++
+     str "     : " ++ prtype_env env typ ++ fnl ())
 
 let print_typed_value x = print_typed_value_in_env (Global.env ()) x
 			  		  
 let print_impl_args = function
-  | []  -> [<>]
-  | [i] -> [< 'sTR"Position ["; 'iNT i; 'sTR"] is implicit" >]
+  | []  -> mt ()
+  | [i] -> str"Position [" ++ int i ++ str"] is implicit"
   | l   -> 
-      [< 'sTR"Positions ["; 
-         prlist_with_sep (fun () -> [< 'sTR";" >]) (fun i -> [< 'iNT i >]) l;
-         'sTR"] are implicit" >]
+      str"Positions [" ++ 
+      prlist_with_sep (fun () -> str " ++") (fun i -> int i) l ++
+      str"] are implicit"
 
 (* To be improved; the type should be used to provide the types in the
    abstractions. This should be done recursively inside prterm, so that
@@ -53,13 +53,13 @@ let print_impl_args = function
 let print_named_def name body typ =
   let pbody = prterm body in
   let ptyp = prtype typ in
-  [< 'sTR "*** ["; 'sTR name ; 'sTR " ";
-     hOV 0 [< 'sTR ":="; 'bRK (1,2); pbody; 'sPC;
-	      'sTR ":"; 'bRK (1,2); ptyp >];
-	   'sTR "]"; 'fNL >]
+  (str "*** [" ++ str name ++ str " " ++
+     hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
+	      str ":" ++ brk (1,2) ++ ptyp) ++
+	   str "]" ++ fnl ())
 
 let print_named_assum name typ =
-  [< 'sTR "*** [" ; 'sTR name ; 'sTR " : "; prtype typ; 'sTR "]"; 'fNL >]
+  (str "*** [" ++ str name ++ str " : " ++ prtype typ ++ str "]" ++ fnl ())
 
 let print_named_decl (id,c,typ) =
   let s = string_of_id id in
@@ -72,35 +72,36 @@ let assumptions_for_print lna =
 
 let implicit_args_id id l = 
   if l = [] then 
-    [<>]
+    (mt ())
   else 
-    [< 'sTR"For "; pr_id id; 'sTR": "; print_impl_args l ; 'fNL >]
+    (str"For " ++ pr_id id ++ str": " ++ print_impl_args l ++ fnl ())
 
 let implicit_args_msg sp mipv = 
-  [< prvecti
+  (prvecti
        (fun i mip -> 
 	  let imps = inductive_implicits_list (sp,i) in
-          [< (implicit_args_id mip.mind_typename imps);
+          ((implicit_args_id mip.mind_typename imps) ++
              prvecti 
 	       (fun j idc ->
 		  let imps = constructor_implicits_list ((sp,i),succ j) in
                   (implicit_args_id idc imps))
                mip.mind_consnames 
-          >])
-       mipv >]
+))
+       mipv)
 
 let print_params env params =
   if List.length params = 0 then 
-    [<>] 
+    (mt ()) 
   else
-    [< 'sTR "["; pr_rel_context env params; 'sTR "]"; 'bRK(1,2) >]
+    (str "[" ++ pr_rel_context env params ++ str "]" ++ brk(1,2))
 
 let print_constructors envpar names types =
   let pc =
-    [< prvect_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >])
-         (fun (id,c) -> [< pr_id id; 'sTR " : "; prterm_env envpar c >])
-	 (array_map2 (fun n t -> (n,t)) names types) >]
-  in hV 0 [< 'sTR "  "; pc >] 
+    prvect_with_sep (fun () -> brk(1,0) ++ str "| ")
+      (fun (id,c) -> pr_id id ++ str " : " ++ prterm_env envpar c)
+      (array_map2 (fun n t -> (n,t)) names types)
+  in 
+  hv 0 (str "  " ++ pc)
 
 let build_inductive sp tyi =
   let (mib,mip) = Global.lookup_inductive (sp,tyi) in
@@ -116,11 +117,11 @@ let print_one_inductive sp tyi =
   let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
   let env = Global.env () in
   let envpar = push_rel_context params env in
-  (hOV 0
-     [< (hOV 0
-	   [< pr_global (IndRef (sp,tyi)) ; 'bRK(1,2); print_params env params;
-	      'sTR ": "; prterm_env envpar arity; 'sTR " :=" >]);
-	'bRK(1,2); print_constructors envpar cstrnames cstrtypes >]) 
+  (hov 0
+     ((hov 0
+	   (pr_global (IndRef (sp,tyi)) ++ brk(1,2) ++ print_params env params ++
+	      str ": " ++ prterm_env envpar arity ++ str " :=")) ++
+	brk(1,2) ++ print_constructors envpar cstrnames cstrtypes)) 
 
 let print_mutual sp =
   let (mib,mip) = Global.lookup_inductive (sp,0) in
@@ -131,13 +132,13 @@ let print_mutual sp =
       if mib.mind_finite then "Inductive " else "CoInductive " in
     let env = Global.env () in
     let envpar = push_rel_context params env in
-    (hOV 0 [< 
-       'sTR sfinite ; 
-      pr_global (IndRef (sp,0)); 'bRK(1,2);
-       print_params env params; 'bRK(1,5);
-       'sTR": "; prterm_env envpar arity; 'sTR" :=";
-       'bRK(0,4); print_constructors envpar cstrnames cstrtypes; 'fNL;
-       implicit_args_msg sp mib.mind_packets  >] )
+    (hov 0 (
+       str sfinite ++ 
+      pr_global (IndRef (sp,0)) ++ brk(1,2) ++
+       print_params env params ++ brk(1,5) ++
+       str": " ++ prterm_env envpar arity ++ str" :=" ++
+       brk(0,4) ++ print_constructors envpar cstrnames cstrtypes ++ fnl () ++
+       implicit_args_msg sp mib.mind_packets) )
   (* Mutual [co]inductive definitions *)
   else
     let _,(mipli,miplc) =
@@ -147,24 +148,24 @@ let print_mutual sp =
         mipv (0,([],[])) 
     in 
     let strind =
-      if mipli = [] then [<>] 
-      else [< 'sTR "Inductive"; 'bRK(1,4);
+      if mipli = [] then (mt ()) 
+      else (str "Inductive" ++ brk(1,4) ++
               (prlist_with_sep
-                 (fun () -> [< 'fNL; 'sTR"  with"; 'bRK(1,4) >])
-                 (print_one_inductive sp) mipli); 'fNL >]
+                 (fun () -> (fnl () ++ str"  with" ++ brk(1,4)))
+                 (print_one_inductive sp) mipli) ++ fnl ())
     and strcoind =
-      if miplc = [] then [<>] 
-      else [< 'sTR "CoInductive"; 'bRK(1,4);
+      if miplc = [] then (mt ()) 
+      else (str "CoInductive" ++ brk(1,4) ++
               (prlist_with_sep
-                 (fun () -> [<'fNL; 'sTR "  with"; 'bRK(1,4) >]) 
-                 (print_one_inductive sp) miplc); 'fNL >] 
+                 (fun () -> (fnl () ++ str "  with" ++ brk(1,4))) 
+                 (print_one_inductive sp) miplc) ++ fnl ()) 
     in
-    (hV 0 [< 'sTR"Mutual " ; 
-             if mib.mind_finite then 
-	       [< strind; strcoind >] 
-             else 
-	       [<strcoind; strind>];
-             implicit_args_msg sp mipv >])
+    (hv 0 (str"Mutual " ++
+           (if mib.mind_finite then 
+	      strind ++ strcoind
+            else 
+	      strcoind ++ strind) ++
+           implicit_args_msg sp mipv))
 
 (*
   let env = Global.env () in
@@ -177,24 +178,24 @@ let print_mutual sp =
   let arities = Array.map (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mipv in
   let env_ar = push_rels lpars env in
   let pr_constructor (id,c) =
-    [< pr_id id; 'sTR " : "; prterm_env env_ar c >] in
+    (pr_id id ++ str " : " ++ prterm_env env_ar c) in
   let print_constructors mis =
     let (_,lC) = mis_type_mconstructs mis in
     let lidC =
       array_map2 (fun id c -> (id, snd (decomp_n_prod env evd nparams c)))
 	(mis_consnames mis) lC in
     let plidC =
-      prvect_with_sep (fun () -> [<'bRK(0,0); 'sTR "| " >])
+      prvect_with_sep (fun () -> (brk(0,0) ++ str "| "))
         pr_constructor
 	lidC
     in
-    hV 0 [< 'sTR "  "; plidC >] 
+    hV 0 (str "  " ++ plidC) 
   in
   let params =
     if nparams = 0 then 
-      [<>] 
+      (mt ()) 
     else
-      [< 'sTR "["; pr_rel_context env lpars; 'sTR "]"; 'bRK(1,2) >] in
+      (str "[" ++ pr_rel_context env lpars ++ str "]" ++ brk(1,2)) in
   let print_oneind tyi =
     let mis =
       build_mis
@@ -203,11 +204,11 @@ let print_mutual sp =
 	mib in
     let (_,arity) = decomp_n_prod env evd nparams
 		      (body_of_type (mis_user_arity mis)) in
-      (hOV 0
-         [< (hOV 0
-	       [< pr_global (IndRef (sp,tyi)) ; 'bRK(1,2); params;
-	          'sTR ": "; prterm_env env_ar arity; 'sTR " :=" >]);
-            'bRK(1,2); print_constructors mis >]) 
+      (hov 0
+         ((hov 0
+	       (pr_global (IndRef (sp,tyi)) ++ brk(1,2) ++ params ++
+	          str ": " ++ prterm_env env_ar arity ++ str " :=")) ++
+            brk(1,2) ++ print_constructors mis)) 
   in 
   let mis0 =
     build_mis
@@ -218,14 +219,14 @@ let print_mutual sp =
     let (_,arity) = decomp_n_prod env evd nparams
 		      (body_of_type (mis_user_arity mis0)) in 
     let sfinite = if mis_finite mis0 then "Inductive " else "CoInductive " in
-    (hOV 0 [< 'sTR sfinite ; pr_global (IndRef (sp,0));
+    (hov 0 (str sfinite ++ pr_global (IndRef (sp,0)) ++
               if nparams = 0 then 
-		[<>] 
+		(mt ()) 
               else 
-		[< 'sTR" ["; pr_rel_context env lpars; 'sTR "]">];
-              'bRK(1,5); 'sTR": "; prterm_env env_ar arity; 'sTR" :=";
-              'bRK(0,4); print_constructors mis0; 'fNL;
-              implicit_args_msg sp mipv  >] )
+		(str" [" ++ pr_rel_context env lpars ++ str "]") ++
+              brk(1,5) ++ str": " ++ prterm_env env_ar arity ++ str" :=" ++
+              brk(0,4) ++ print_constructors mis0 ++ fnl () ++
+              implicit_args_msg sp mipv) )
   (* Mutual [co]inductive definitions *)
   else
     let _,(mipli,miplc) =
@@ -235,63 +236,63 @@ let print_mutual sp =
         (0,([],[])) (Array.to_list mipv) 
     in 
     let strind =
-      if mipli = [] then [<>] 
-      else [< 'sTR "Inductive"; 'bRK(1,4);
+      if mipli = [] then (mt ()) 
+      else (str "Inductive" ++ brk(1,4) ++
               (prlist_with_sep
-                 (fun () -> [< 'fNL; 'sTR"  with"; 'bRK(1,4) >])
+                 (fun () -> (fnl () ++ str"  with" ++ brk(1,4)))
                  print_oneind
-                 (List.rev mipli)); 'fNL >]
+                 (List.rev mipli)) ++ fnl ())
     and strcoind =
-      if miplc = [] then [<>] 
-      else [< 'sTR "CoInductive"; 'bRK(1,4);
+      if miplc = [] then (mt ()) 
+      else (str "CoInductive" ++ brk(1,4) ++
               (prlist_with_sep
-                 (fun () -> [<'fNL; 'sTR "  with"; 'bRK(1,4) >]) 
-                 print_oneind (List.rev miplc)); 'fNL >] 
+                 (fun () -> (fnl () ++ str "  with" ++ brk(1,4))) 
+                 print_oneind (List.rev miplc)) ++ fnl ()) 
     in
-    (hV 0 [< 'sTR"Mutual " ; 
+    (hV 0 (str"Mutual " ++ 
              if mis_finite mis0 then 
-	       [< strind; strcoind >] 
+	       (strind ++ strcoind) 
              else 
-	       [<strcoind; strind>];
-             implicit_args_msg sp mipv >])
+	       (strcoind ++ strind) ++
+             implicit_args_msg sp mipv))
 *)
 let print_section_variable sp =
   let (d,_) = get_variable sp in
   let l = implicits_of_var sp in
-  [< print_named_decl d; print_impl_args l; 'fNL >]
+  (print_named_decl d ++ print_impl_args l ++ fnl ())
 
 let print_body = function
   | Some c  -> prterm c
-  | None -> [< 'sTR"<no body>" >]
+  | None -> (str"<no body>")
 
 let print_typed_body (val_0,typ) =
-  [< print_body val_0; 'fNL; 'sTR "     : "; prtype typ; 'fNL >]
+  (print_body val_0 ++ fnl () ++ str "     : " ++ prtype typ ++ fnl ())
 
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = cb.const_body in
   let typ = cb.const_type in
   let impls = constant_implicits_list sp in
-  hOV 0 [< (match val_0 with 
+  hov 0 ((match val_0 with 
 		| None -> 
-		    [< 'sTR"*** [ "; 
-		       print_basename sp;  
-		       'sTR " : "; 'cUT ; prtype typ ; 'sTR" ]"; 'fNL >]
+		    (str"*** [ " ++ 
+		       print_basename sp ++  
+		       str " : " ++ cut () ++ prtype typ ++ str" ]" ++ fnl ())
 		| _ -> 
-		    [< print_basename sp; 
-		       'sTR sep; 'cUT ;
+		    (print_basename sp ++ 
+		       str sep ++ cut () ++
 		       if with_values then 
 			 print_typed_body (val_0,typ) 
 		       else 
-			 [< prtype typ ; 'fNL >] >]); 
-	     print_impl_args impls; 'fNL >]
+			 (prtype typ ++ fnl ()))) ++ 
+	     print_impl_args impls ++ fnl ())
 
-let print_inductive sp = [< print_mutual sp; 'fNL >]
+let print_inductive sp = (print_mutual sp ++ fnl ())
 
 let print_syntactic_def sep sp =
   let id = basename sp in
   let c = Syntax_def.search_syntactic_definition sp in 
-  [< 'sTR" Syntactif Definition "; pr_id id ; 'sTR sep; pr_rawterm c; 'fNL >]
+  (str" Syntactif Definition " ++ pr_id id ++ str sep ++ pr_rawterm c ++ fnl ())
 
 let print_leaf_entry with_values sep (sp,lobj) =
   let tag = object_tag lobj in
@@ -303,56 +304,56 @@ let print_leaf_entry with_values sep (sp,lobj) =
     | (_,"INDUCTIVE") ->
 	print_inductive sp
     | (_,"AUTOHINT") -> 
-(*	[< 'sTR" Hint Marker"; 'fNL >]*)
-	[< >]
+(*	(str" Hint Marker" ++ fnl ())*)
+	(mt ())
     | (_,"GRAMMAR") -> 
-(*	[< 'sTR" Grammar Marker"; 'fNL >]*)
-	[< >]
+(*	(str" Grammar Marker" ++ fnl ())*)
+	(mt ())
     | (_,"SYNTAXCONSTANT") -> 
 	print_syntactic_def sep sp
     | (_,"PPSYNTAX") -> 
-(*	[< 'sTR" Syntax Marker"; 'fNL >]*)
-	[< >]
+(*	(str" Syntax Marker" ++ fnl ())*)
+	(mt ())
     | (_,"TOKEN") -> 
-(*	[< 'sTR" Token Marker"; 'fNL >]*)
-	[< >]
+(*	(str" Token Marker" ++ fnl ())*)
+	(mt ())
     | (_,"CLASS") -> 
-(*	[< 'sTR" Class Marker"; 'fNL >]*)
-	[< >]
+(*	(str" Class Marker" ++ fnl ())*)
+	(mt ())
     | (_,"COERCION") -> 
-(*	[< 'sTR" Coercion Marker"; 'fNL >]*)
-	[< >]
+(*	(str" Coercion Marker" ++ fnl ())*)
+	(mt ())
     | (_,"REQUIRE") -> 
-(*	[< 'sTR" Require Marker"; 'fNL >]*)
-	[< >]
-    | (_,"END-SECTION") -> [< >]
-    | (_,"STRUCTURE") -> [< >]
+(*	(str" Require Marker" ++ fnl ())*)
+	(mt ())
+    | (_,"END-SECTION") -> (mt ())
+    | (_,"STRUCTURE") -> (mt ())
 (* To deal with forgotten cases... *)
-    | (_,s) -> [< >]
+    | (_,s) -> (mt ())
 (*
     | (_,s) -> 
-	[< 'sTR(string_of_path sp); 'sTR" : ";
-           'sTR"Unrecognized object "; 'sTR s; 'fNL >]
+	(str(string_of_path sp) ++ str" : " ++
+           str"Unrecognized object " ++ str s ++ fnl ())
 *)
 
 let rec print_library_entry with_values ent = 
   let sep = if with_values then " = " else " : " in 
   match ent with
     | (sp,Lib.Leaf lobj) -> 
-	[< print_leaf_entry with_values sep (sp,lobj) >]
+	(print_leaf_entry with_values sep (sp,lobj))
     | (sp,Lib.OpenedSection (dir,_)) -> 
-        [< 'sTR " >>>>>>> Section "; pr_id (basename sp); 'fNL >]
+        (str " >>>>>>> Section " ++ pr_id (basename sp) ++ fnl ())
     | (sp,Lib.ClosedSection _) -> 
-        [< 'sTR " >>>>>>> Closed Section "; pr_id (basename sp); 'fNL >]
+        (str " >>>>>>> Closed Section " ++ pr_id (basename sp) ++ fnl ())
     | (_,Lib.Module dir) ->
-	[< 'sTR " >>>>>>> Module "; pr_dirpath dir; 'fNL >]
+	(str " >>>>>>> Module " ++ pr_dirpath dir ++ fnl ())
     | (_,Lib.FrozenState _) ->
-	[< >]
+	(mt ())
 	
 and print_context with_values = 
   let rec prec = function
-    | h::rest -> [< prec rest ; print_library_entry with_values h >]
-    | [] -> [< >]
+    | h::rest -> (prec rest ++ print_library_entry with_values h)
+    | [] -> (mt ())
   in 
   prec
 
@@ -405,7 +406,7 @@ let print_safe_judgment env j =
     
 let print_eval red_fun env {uj_val=trm;uj_type=typ} =
   let ntrm = red_fun env Evd.empty trm in
-  [< 'sTR "     = "; print_judgment env {uj_val = ntrm; uj_type = typ} >]
+  (str "     = " ++ print_judgment env {uj_val = ntrm; uj_type = typ})
 
 let print_name qid = 
   try 
@@ -431,14 +432,14 @@ let print_name qid =
     let dir,str = repr_qualid qid in 
     if (repr_dirpath dir) <> [] then raise Not_found;
     let (_,c,typ) = Global.lookup_named str in 
-    [< print_named_decl (str,c,typ) >]
+    (print_named_decl (str,c,typ))
   with Not_found ->
   try
     let sp = Syntax_def.locate_syntactic_definition qid in
     print_syntactic_def " = " sp
   with Not_found ->
     errorlabstrm "print_name"
-      [< pr_qualid qid; 'sPC; 'sTR "not a defined object" >]
+      (pr_qualid qid ++ spc () ++ str "not a defined object")
 
 let print_opaque_name qid = 
   let sigma = Evd.empty in
@@ -464,17 +465,17 @@ let print_opaque_name qid =
       | _ -> 
 	  assert false
   with Not_found -> 
-    errorlabstrm "print_opaque" [< pr_qualid qid; 'sPC; 'sTR "not declared" >]
+    errorlabstrm "print_opaque" (pr_qualid qid ++ spc () ++ str "not declared")
 
 let print_local_context () =
   let env = Lib.contents_after None in
   let rec print_var_rec = function 
-    | [] -> [< >]
+    | [] -> (mt ())
     | (sp,Lib.Leaf lobj)::rest ->
 	if "VARIABLE" = object_tag lobj then
           let (d,_) = get_variable (basename sp) in 
-	  [< print_var_rec rest;
-             print_named_decl d >]
+	  (print_var_rec rest ++
+             print_named_decl d)
 	else 
 	  print_var_rec rest
     | _::rest -> print_var_rec rest
@@ -485,22 +486,22 @@ let print_local_context () =
            | "CONSTANT" | "PARAMETER" -> 
                let {const_body=val_0;const_type=typ} = 
 		 Global.lookup_constant sp in
-               [< print_last_const rest;
-                  print_basename sp ;'sTR" = ";
-                  print_typed_body (val_0,typ) >]
+               (print_last_const rest ++
+                  print_basename sp ++str" = " ++
+                  print_typed_body (val_0,typ))
            | "INDUCTIVE" -> 
-               [< print_last_const rest;print_mutual sp; 'fNL >]
-           | "VARIABLE" ->  [< >]
+               (print_last_const rest ++print_mutual sp ++ fnl ())
+           | "VARIABLE" ->  (mt ())
            | _          ->  print_last_const rest)
-    | _ -> [< >]
+    | _ -> (mt ())
   in 
-  [< print_var_rec env;  print_last_const env >]
+  (print_var_rec env ++  print_last_const env)
 
 let fprint_var name typ =
-  [< 'sTR ("*** [" ^ name ^ " :"); fprtype typ; 'sTR "]"; 'fNL >]
+  (str ("*** [" ^ name ^ " :") ++ fprtype typ ++ str "]" ++ fnl ())
 
 let fprint_judge {uj_val=trm;uj_type=typ} = 
-  [< fprterm trm; 'sTR" : " ; fprterm (body_of_type typ) >]
+  (fprterm trm ++ str" : " ++ fprterm (body_of_type typ))
 
 let unfold_head_fconst = 
   let rec unfrec k = match kind_of_term k with
@@ -541,37 +542,37 @@ let print_index_coercion c =
 
 let print_class i =
   let cl,_ = class_info_from_index i in
-  [< 'sTR (string_of_class cl) >]
+  (str (string_of_class cl))
   
 let print_path ((i,j),p) = 
-  [< 'sTR"["; 
-     prlist_with_sep (fun () -> [< 'sTR"; " >])
-       (fun c ->  print_index_coercion c) p;
-     'sTR"] : "; print_class i; 'sTR" >-> ";
-     print_class j >]
+  (str"[" ++ 
+     prlist_with_sep (fun () -> (str"; "))
+       (fun c ->  print_index_coercion c) p ++
+     str"] : " ++ print_class i ++ str" >-> " ++
+     print_class j)
 
 let _ = Classops.install_path_printer print_path
 
 let print_graph () = 
-  [< prlist_with_sep pr_fnl print_path (inheritance_graph()) >]
+  (prlist_with_sep pr_fnl print_path (inheritance_graph()))
 
 let print_classes () = 
-  [< prlist_with_sep pr_spc
+  (prlist_with_sep pr_spc
        (fun (_,(cl,x)) -> 
-          [< 'sTR (string_of_class cl)
-	       (*; 'sTR(string_of_strength x.cl_strength) *) >]) 
-       (classes()) >]
+          (str (string_of_class cl)
+	       (* ++ str(string_of_strength x.cl_strength) *))) 
+       (classes()))
 
 let print_coercions () = 
-  [< prlist_with_sep pr_spc
-       (fun (_,(_,v)) -> [< print_coercion_value v >]) (coercions()) >]
+  (prlist_with_sep pr_spc
+       (fun (_,(_,v)) -> (print_coercion_value v)) (coercions()))
   
 let index_of_class cl =
   try 
     fst (class_info cl)
   with _ -> 
     errorlabstrm "index_of_class"
-      [< 'sTR(string_of_class cl); 'sTR" is not a defined class" >]
+      (str(string_of_class cl) ++ str" is not a defined class")
 
 let print_path_between cls clt = 
   let i = index_of_class cls in
@@ -581,8 +582,8 @@ let print_path_between cls clt =
       lookup_path_between (i,j) 
     with _ -> 
       errorlabstrm "index_cl_of_id"
-        [< 'sTR"No path between ";'sTR(string_of_class cls); 
-	   'sTR" and ";'sTR(string_of_class clt) >]
+        (str"No path between " ++str(string_of_class cls) ++ 
+	   str" and " ++str(string_of_class clt))
   in
   print_path ((i,j),p)
 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 77d0f59a1d..3076213e59 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -25,29 +25,29 @@ open Nametab
 
 let emacs_str s = if !Options.print_emacs then s else "" 
 
-let dfltpr ast = [< 'sTR"#GENTERM " ; print_ast ast >];;
+let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;
 
 let pr_global ref = pr_global_env (Global.env()) ref
 
 let global_const_name sp =
   try pr_global (ConstRef sp)
   with Not_found -> (* May happen in debug *)
-    [< 'sTR ("CONST("^(string_of_path sp)^")") >]
+    (str ("CONST("^(string_of_path sp)^")"))
 
 let global_ind_name (sp,tyi) =
   try pr_global (IndRef (sp,tyi))
   with Not_found -> (* May happen in debug *)
-    [< 'sTR ("IND("^(string_of_path sp)^","^(string_of_int tyi)^")") >]
+    (str ("IND("^(string_of_path sp)^","^(string_of_int tyi)^")"))
 
 let global_constr_name ((sp,tyi),i) =
   try pr_global (ConstructRef ((sp,tyi),i))
   with Not_found -> (* May happen in debug *)
-    [< 'sTR ("CONSTRUCT("^(string_of_path sp)^","^(string_of_int tyi)
-		  ^","^(string_of_int i)^")") >]
+    (str ("CONSTRUCT("^(string_of_path sp)^","^(string_of_int tyi)
+		  ^","^(string_of_int i)^")"))
 
 let globpr gt = match gt with
-  | Nvar(_,s) -> [< pr_id s >]
-  | Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
+  | Nvar(_,s) -> (pr_id s)
+  | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
   | Node(_,"CONST",[Path(_,sl)]) ->
       global_const_name (section_path sl)
   | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
@@ -55,16 +55,16 @@ let globpr gt = match gt with
   | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
       global_constr_name ((section_path sl, tyi), i)
   | Dynamic(_,d) ->
-    if (Dyn.tag d) = "constr" then [< 'sTR"<dynamic [constr]>" >]
+    if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>")
     else dfltpr gt
   | gt -> dfltpr gt
 
 let wrap_exception = function
     Anomaly (s1,s2) ->
-      warning ("Anomaly ("^s1^")");pP s2;
-      [< 'sTR"<PP error: non-printable term>" >]
+      warning ("Anomaly ("^s1^")"); pp s2;
+      str"<PP error: non-printable term>"
   | Failure _ | UserError _ | Not_found ->
-      [< 'sTR"<PP error: non-printable term>" >]
+      str"<PP error: non-printable term>"
   | s -> raise s
 
 (* These are the names of the universes where the pp rules for constr and
@@ -135,10 +135,10 @@ let rec gentacpr gt =
   Esyntax.genprint default_tacpr tactic_syntax_universe tactic_initial_prec gt
 
 and default_tacpr = function
-    | Nvar(_,s) -> [< pr_id s >]
+    | Nvar(_,s) -> (pr_id s)
 
     (* constr's may occur inside tac expressions ! *)
-    | Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
+    | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
     | Node(_,"CONST",[Path(_,sl)]) ->
 	let sp = section_path sl in
 	pr_global (ConstRef sp)
@@ -150,39 +150,39 @@ and default_tacpr = function
 	pr_global (ConstructRef ((sp,tyi),i))
 
     (* This should be tactics *)
-    | Node(_,s,[]) -> [< 'sTR s >]
+    | Node(_,s,[]) -> (str s)
     | Node(_,s,ta) ->
-	[< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gentacpr ta) >]
+	(str s ++ brk(1,2) ++ hov 0 (prlist_with_sep pr_spc gentacpr ta))
     | Dynamic(_,d) as gt ->
       let tg = Dyn.tag d in
-      if tg = "tactic" then [< 'sTR"<dynamic [tactic]>" >]
-      else if tg = "value" then [< 'sTR"<dynamic [value]>" >]
-      else if tg = "constr" then [< 'sTR"<dynamic [constr]>" >]
+      if tg = "tactic" then (str"<dynamic [tactic]>")
+      else if tg = "value" then (str"<dynamic [value]>")
+      else if tg = "constr" then (str"<dynamic [constr]>")
       else dfltpr gt
     | gt -> dfltpr gt 
 
 let pr_var_decl env (id,c,typ) =
   let pbody = match c with
-    | None ->  [<  >]
+    | None ->  (mt ())
     | Some c ->
 	(* Force evaluation *) 
 	let pb = prterm_env env c in
-	[< 'sTR" := "; pb >] in
+	(str" := " ++ pb) in
   let pt = prtype_env env typ in
-  let ptyp = [< 'sTR" : "; pt >] in
-  [< pr_id id ; hOV 0 [< pbody; ptyp >] >]
+  let ptyp = (str" : " ++ pt) in
+  (pr_id id ++ hov 0 (pbody ++ ptyp))
 
 let pr_rel_decl env (na,c,typ) =
   let pbody = match c with
-    | None ->  [<  >]
+    | None ->  (mt ())
     | Some c ->
 	(* Force evaluation *) 
 	let pb = prterm_env env c in
-	[< 'sTR":="; 'sPC; pb; 'sPC >] in
+	(str":=" ++ spc () ++ pb ++ spc ()) in
   let ptyp = prtype_env env typ in
   match na with
-    | Anonymous -> [< 'sTR"<>" ; 'sPC; pbody; 'sTR":"; 'sPC; ptyp >]
-    | Name id -> [< pr_id id ; 'sPC; pbody; 'sTR":"; 'sPC; ptyp >]
+    | Anonymous -> (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+    | Name id -> (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
 
 
 (* Prints out an "env" in a nice format.  We print out the
@@ -191,18 +191,18 @@ let pr_rel_decl env (na,c,typ) =
 
 (* Prints a signature, all declarations on the same line if possible *)
 let pr_named_context_of env =
-  hV 0 [< (fold_named_context
-	     (fun env d pps -> [< pps; 'wS 2; pr_var_decl env d >])
-             env) [< >] >]
+  hv 0 (fold_named_context
+	  (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d)
+          env ~init:(mt ()))
 
 let pr_rel_context env rel_context =
   let rec prec env = function
-    | [] -> [<>] 
+    | [] -> (mt ()) 
     | [b] -> pr_rel_decl env b
     | b::rest ->
         let pb = pr_rel_decl env b in
         let penvtl = prec (push_rel b env) rest in
-        [< pb; 'sTR";"; 'sPC; penvtl >]
+        (pb ++ str";" ++ spc () ++ penvtl)
   in 
   prec env (List.rev rel_context)
 
@@ -211,21 +211,21 @@ let pr_context_unlimited env =
   let sign_env =
     fold_named_context
       (fun env d pps ->
-         let pidt =  pr_var_decl env d in [< pps; 'fNL; pidt >])
-      env [< >] 
+         let pidt =  pr_var_decl env d in (pps ++ fnl () ++ pidt))
+      env ~init:(mt ()) 
   in
   let db_env =
     fold_rel_context
       (fun env d pps ->
-         let pnat = pr_rel_decl env d in [< pps; 'fNL; pnat >])
-      env [< >]
+         let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat))
+      env ~init:(mt ())
   in 
-  [< sign_env; db_env >]
+  (sign_env ++ db_env)
 
 let pr_ne_context_of header env =
   if Environ.rel_context env = empty_rel_context &
-    Environ.named_context env = empty_named_context  then [< >]
-  else let penv = pr_context_unlimited env in [< header; penv; 'fNL >]
+    Environ.named_context env = empty_named_context  then (mt ())
+  else let penv = pr_context_unlimited env in (header ++ penv ++ fnl ())
 
 let pr_context_limit n env =
   let named_context = Environ.named_context env in
@@ -238,25 +238,25 @@ let pr_context_limit n env =
       fold_named_context
         (fun env d (i,pps) ->
            if i < k then 
-	     (i+1, [< pps ;'sTR "." >])
+	     (i+1, (pps ++str "."))
 	   else
              let pidt = pr_var_decl env d in
-	     (i+1, [< pps ; 'fNL ;
-		      'sTR (emacs_str (String.make 1 (Char.chr 253)));
-		      pidt >]))
-        env (0,[< >]) 
+	     (i+1, (pps ++ fnl () ++
+		      str (emacs_str (String.make 1 (Char.chr 253))) ++
+		      pidt)))
+        env ~init:(0,(mt ())) 
     in
     let db_env =
       fold_rel_context
         (fun env d pps ->
            let pnat = pr_rel_decl env d in
-	   [< pps; 'fNL;
-	      'sTR (emacs_str (String.make 1 (Char.chr 253)));
-	      pnat >])
-        env [< >]
+	   (pps ++ fnl () ++
+	      str (emacs_str (String.make 1 (Char.chr 253))) ++
+	      pnat))
+        env ~init:(mt ())
     in 
-    [< sign_env; db_env >]
+    (sign_env ++ db_env)
 
 let pr_context_of env = match Options.print_hyps_limit () with 
-  | None -> hV 0 (pr_context_unlimited env)
-  | Some n -> hV 0 (pr_context_limit n env)
+  | None -> hv 0 (pr_context_unlimited env)
+  | Some n -> hv 0 (pr_context_limit n env)
diff --git a/parsing/search.ml b/parsing/search.ml
index a96567bf44..1d5619969f 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -80,7 +80,7 @@ let crible (fn : global_reference -> env -> constr -> unit) ref =
     Library.iter_all_segments false crible_rec 
   with Not_found -> 
     errorlabstrm "search"
-      [< pr_global ref; 'sPC; 'sTR "not declared" >]
+      (pr_global ref ++ spc () ++ str "not declared")
 
 (* Fine Search. By Yves Bertot. *)
 
@@ -101,7 +101,7 @@ let xor a b = (a or b) & (not (a & b))
 let plain_display ref a c =
   let pc = prterm_env a c in
   let pr = pr_global ref in
-  mSG [< hOV 2 [< pr; 'sTR":"; 'sPC; pc >]; 'fNL>]
+  msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ())
 
 let filter_by_module (module_list:dir_path list) (accept:bool) 
   (ref:global_reference) (env:env) _ =
diff --git a/parsing/termast.ml b/parsing/termast.ml
index fb9852f3b4..f7affb5b10 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -278,7 +278,7 @@ and ast_of_eqn (_,ids,pl,c) =
   ope("EQN", (ast_of_raw c)::(List.map ast_of_cases_pattern pl))
 
 and ast_of_rawopt = function
-  | None -> (str "SYNTH")
+  | None -> (string "SYNTH")
   | Some p -> ast_of_raw p
 
 and factorize_binder n oper na aty c =
@@ -399,7 +399,7 @@ let rec ast_of_pattern env = function
   | PCoFix c -> ast_of_raw (Detyping.detype [] env (mkCoFix c))
 	
 and ast_of_patopt env = function
-  | None -> (str "SYNTH")
+  | None -> (string "SYNTH")
   | Some p -> ast_of_pattern env p
 
 and factorize_binder_pattern env n oper na aty c =