compat ocaml 3.03

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

8 files changed, 265 insertions, 266 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index d73264e924..1a2ebd32ff 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -430,8 +430,8 @@ let clenv_assign mv rhs clenv =
 	       (* Streams are lazy, force evaluation of id to catch Not_found*)
 	       let id = Intmap.find mv clenv.namenv in
 	       errorlabstrm "clenv_assign"
-		 [< 'sTR "An incompatible instantiation has already been found for "; 
-		    pr_id id >]
+		 (str "An incompatible instantiation has already been found for " ++ 
+		    pr_id id)
 	     with Not_found ->
 	       anomaly "clenv_assign: non dependent metavar already assigned"
 	   else
@@ -907,7 +907,7 @@ let clenv_lookup_name clenv id =
   match intmap_inv clenv.namenv id with
     | []  -> 
 	errorlabstrm "clenv_lookup_name"
-          [< 'sTR"No such bound variable "; pr_id id >]
+          (str"No such bound variable " ++ pr_id id)
     | [n] -> 
 	n
     |  _  -> 
@@ -926,18 +926,18 @@ let clenv_match_args s clause =
              | Dep s ->
 		 if List.mem_assoc b t then 
 		   errorlabstrm "clenv_match_args" 
-		     [< 'sTR "The variable "; pr_id s; 
-			'sTR " occurs more than once in binding" >]
+		     (str "The variable " ++ pr_id s ++ 
+			str " occurs more than once in binding")
 		 else
 		   clenv_lookup_name clause s
 	     | NoDep n ->
 		 if List.mem_assoc b t then errorlabstrm "clenv_match_args"
-		   [< 'sTR "The position "; 'iNT n ;
-		      'sTR " occurs more than once in binding" >];
+		   (str "The position " ++ int n ++
+		      str " occurs more than once in binding");
 		 (try 
 		    List.nth mvs (n-1)
 		  with Failure "item" -> errorlabstrm "clenv_match_args"
-                      [< 'sTR"No such binder" >])
+                      (str"No such binder"))
 	     | Com -> anomaly "No free term in clenv_match_args")
 	in
 	let k_typ = w_hnf_constr clause.hook (clenv_instance_type clause k)
@@ -1092,7 +1092,7 @@ let make_clenv_binding_apply wc n (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 make_clenv_binding wc (c,t) lbind = 
   let largs    = collect_com lbind in
@@ -1105,7 +1105,7 @@ let make_clenv_binding 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")
 
 open Printer
 
@@ -1113,15 +1113,15 @@ let pr_clenv clenv =
   let pr_name mv =
     try 
       let id = Intmap.find mv clenv.namenv in
-      [< 'sTR"[" ; pr_id id ; 'sTR"]" >]
-    with Not_found -> [< >]
+      (str"[" ++ pr_id id ++ str"]")
+    with Not_found -> (mt ())
   in
   let pr_meta_binding = function
     | (mv,Cltyp b) ->
-      	hOV 0 [< 'iNT mv ; pr_name mv ; 'sTR " : " ; prterm b.rebus ; 'fNL >]
+      	hov 0 (int mv ++ pr_name mv ++ str " : " ++ prterm b.rebus ++ fnl ())
     | (mv,Clval(b,_)) ->
-      	hOV 0 [< 'iNT mv ; pr_name mv ; 'sTR " := " ; prterm b.rebus ; 'fNL >]
+      	hov 0 (int mv ++ pr_name mv ++ str " := " ++ prterm b.rebus ++ fnl ())
   in
-  [< 'sTR"TEMPL: " ; prterm clenv.templval.rebus ;
-     'sTR" : " ; prterm clenv.templtyp.rebus ; 'fNL ;
-     (prlist pr_meta_binding (intmap_to_list clenv.env)) >]
+  (str"TEMPL: " ++ prterm clenv.templval.rebus ++
+     str" : " ++ prterm clenv.templtyp.rebus ++ fnl () ++
+     (prlist pr_meta_binding (intmap_to_list clenv.env)))
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 61edd06bf6..ea524791a4 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -180,8 +180,8 @@ and mk_casegoals sigma goal goalacc p c =
 
 let error_use_instantiate () =
   errorlabstrm "Logic.prim_refiner"
-    [< 'sTR"cannot intro when there are open metavars in the domain type";
-       'sPC; 'sTR"- use Instantiate" >]
+    (str"cannot intro when there are open metavars in the domain type" ++
+       spc () ++ str"- use Instantiate")
     
 (* Auxiliary functions for primitive MOVE tactic
  *
@@ -257,7 +257,7 @@ let apply_to_hyp2 env id f =
 	   found := true; f env d tail
 	 end else 
 	   push_named_decl d env)
-      (named_context env) (reset_context env)
+      (named_context env) ~init:(reset_context env)
   in
   if (not !check) || !found then env' else error "No such assumption"
 
@@ -363,7 +363,7 @@ let remove_hyp_body env sigma id =
                               let b' = mkCast (b,t) in
                               recheck_typability (Some id',id) env'' sigma b');
                        push_named_decl d env'')
-                    tail env');
+                    tail ~init:env');
              env')
 
 (* Primitive tactics are handled here *)
@@ -667,67 +667,67 @@ open Printer
 
 let pr_prim_rule = function
   | {name=Intro;newids=[id]} -> 
-      [< 'sTR"Intro " ; pr_id id >]
+      str"Intro " ++ pr_id id
 	
   | {name=Intro_after;newids=[id]} -> 
-      [< 'sTR"intro after " ; pr_id id >]
+      str"intro after "  ++ pr_id id
 	
   | {name=Intro_replacing;newids=[id]} -> 
-      [< 'sTR"intro replacing " ; pr_id id >]
+      (str"intro replacing "  ++ pr_id id)
 	
   | {name=Cut b;terms=[t];newids=[id]} ->
       if b then
-        [< 'sTR"TrueCut "; prterm t >]
+        (str"TrueCut " ++ prterm t)
       else
-        [< 'sTR"Cut "; prterm t; 'sTR ";[Intro "; pr_id id; 'sTR "|Idtac]" >]
+        (str"Cut " ++ prterm t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]")
 	
   | {name=FixRule;newids=[f];params=[Num(_,n)]} -> 
-      [< 'sTR"Fix "; pr_id f; 'sTR"/"; 'iNT n>]
+      (str"Fix " ++ pr_id f ++ str"/" ++ int n)
       
   | {name=FixRule;newids=(f::lf);params=(Num(_,n))::ln;terms=lar} -> 
       let rec print_mut = 
         function (f::lf),((Num(_,n))::ln),(ar::lar) -> 
-          [< pr_id f; 'sTR"/"; 'iNT n; 'sTR" : "; prterm ar;
-             print_mut (lf,ln,lar)>]
-          | _ -> [<>] in
-      [< 'sTR"Fix "; pr_id f; 'sTR"/"; 'iNT n;
-         'sTR" with "; print_mut (lf,ln,lar) >]
+          pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++
+          print_mut (lf,ln,lar)
+          | _ -> (mt ()) in
+      (str"Fix " ++ pr_id f ++ str"/" ++ int n ++
+         str" with " ++ print_mut (lf,ln,lar))
       
   | {name=Cofix;newids=[f];terms=[]} -> 
-      [< 'sTR"Cofix "; pr_id f >]
+      (str"Cofix " ++ pr_id f)
       
   | {name=Cofix;newids=(f::lf);terms=lar} -> 
       let rec print_mut = 
         function (f::lf),(ar::lar) -> 
-	  [< pr_id f; 'sTR" : "; prterm ar; print_mut (lf,lar)>]
-          | _ -> [<>] 
+	  (pr_id f ++ str" : " ++ prterm ar ++ print_mut (lf,lar))
+          | _ -> (mt ()) 
       in
-      [< 'sTR"Cofix "; pr_id f;  'sTR" with "; print_mut (lf,lar) >]
+      (str"Cofix " ++ pr_id f ++  str" with " ++ print_mut (lf,lar))
 
   | {name=Refine;terms=[c]} -> 
-      [< 'sTR(if occur_meta c then "Refine " else "Exact ") ; prterm c >]
+      (str(if occur_meta c then "Refine " else "Exact ")  ++ prterm c)
       
   | {name=Convert_concl;terms=[c]} ->
-      [< 'sTR"Change " ; prterm c >]
+      (str"Change "  ++ prterm c)
       
   | {name=Convert_hyp;hypspecs=[id];terms=[c]} ->
-      [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >]
+      (str"Change "  ++ prterm c  ++ spc ()  ++ str"in "  ++ pr_id id)
       
   | {name=Convert_defbody;hypspecs=[id];terms=[c]} ->
-      [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >]
+      (str"Change "  ++ prterm c  ++ spc ()  ++ str"in "  ++ pr_id id)
 
   | {name=Convert_deftype;hypspecs=[id];terms=[c]} ->
-      [< 'sTR"Change " ; prterm c ; 'sPC ;
-	 'sTR"in (Type of " ; pr_id id; 'sTR ")" >]
+      (str"Change "  ++ prterm c  ++ spc ()  ++
+	 str"in (Type of "  ++ pr_id id ++ str ")")
       
   | {name=Thin;hypspecs=ids} ->
-      [< 'sTR"Clear " ; prlist_with_sep pr_spc pr_id ids >]
+      (str"Clear "  ++ prlist_with_sep pr_spc pr_id ids)
       
   | {name=ThinBody;hypspecs=ids} ->
-      [< 'sTR"ClearBody " ; prlist_with_sep pr_spc pr_id ids >]
+      (str"ClearBody "  ++ prlist_with_sep pr_spc pr_id ids)
       
   | {name=Move withdep;hypspecs=[id1;id2]} ->
-      [< 'sTR (if withdep then "Dependent " else "");
-	 'sTR"Move " ; pr_id id1; 'sTR " after "; pr_id id2 >]
+      (str (if withdep then "Dependent " else "") ++
+	 str"Move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)
       
   | _ -> anomaly "pr_prim_rule: Unrecognized primitive rule"
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b148c019af..610e99b9f8 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -43,13 +43,13 @@ let get_all_proof_names () = Edit.dom proof_edits
 
 let msg_proofs use_resume =
   match Edit.dom proof_edits with
-    | [] -> [< 'sPC ; 'sTR"(No proof-editing in progress)." >]
-    | l ->  [< 'sTR"." ; 'fNL ; 'sTR"Proofs currently edited:" ; 'sPC ;
-               (prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ;
-	       'sTR"." ;
-               (if use_resume then [< 'fNL ; 'sTR"Use \"Resume\" first." >]
-              	else [< >])
-            >]
+    | [] -> (spc () ++ str"(No proof-editing in progress).")
+    | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
+               (prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ++
+	       str"." ++
+               (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
+              	else (mt ()))
+)
 
 let undo_default = 12
 let undo_limit = ref undo_default
@@ -61,7 +61,7 @@ let undo_limit = ref undo_default
 let get_state () =
   match Edit.read proof_edits with
     | None -> errorlabstrm "Pfedit.get_state"
-          [< 'sTR"No focused proof"; msg_proofs true >]
+          (str"No focused proof" ++ msg_proofs true)
     | Some(_,pfs,ts) -> (pfs,ts)
 
 let get_topstate ()    = snd(get_state())
@@ -79,7 +79,7 @@ let set_current_proof s =
     Edit.focus proof_edits s
   with Invalid_argument "Edit.focus" ->
     errorlabstrm "Pfedit.set_proof"
-      [< 'sTR"No such proof" ; (msg_proofs false) >]
+      (str"No such proof" ++ (msg_proofs false))
 
 let resume_proof = set_current_proof
 
@@ -88,12 +88,12 @@ let suspend_proof () =
     Edit.unfocus proof_edits
   with Invalid_argument "Edit.unfocus" ->
     errorlabstrm "Pfedit.suspend_current_proof"
-      [< 'sTR"No active proof" ; (msg_proofs true) >]
+      (str"No active proof" ++ (msg_proofs true))
       
 let resume_last_proof () =
   match (Edit.last_focused proof_edits) with
     | None ->
-        errorlabstrm "resume_last" [< 'sTR"No proof-editing in progress." >]
+        errorlabstrm "resume_last" (str"No proof-editing in progress.")
     | Some p -> 
 	Edit.focus proof_edits p
 	  
@@ -101,7 +101,7 @@ let get_current_proof_name () =
   match Edit.read proof_edits with
     | None ->
         errorlabstrm "Pfedit.get_proof"
-          [< 'sTR"No focused proof" ; msg_proofs true >]
+          (str"No focused proof" ++ msg_proofs true)
     | Some(na,_,_) -> na
 
 let add_proof (na,pfs,ts) =
@@ -112,7 +112,7 @@ let delete_proof na =
     Edit.delete proof_edits na
   with (UserError ("Edit.delete",_)) ->
     errorlabstrm "Pfedit.delete_proof"
-      [< 'sTR"No such proof" ; msg_proofs false >]
+      (str"No such proof" ++ msg_proofs false)
       
 let init_proofs () = Edit.clear proof_edits
 		       
@@ -121,7 +121,7 @@ let mutate f =
     Edit.mutate proof_edits (fun _ pfs -> f pfs)
   with Invalid_argument "Edit.mutate" ->
     errorlabstrm "Pfedit.mutate"
-      [< 'sTR"No focused proof" ; msg_proofs true >]
+      (str"No focused proof" ++ msg_proofs true)
 
 let start (na,ts) =
   let pfs = mk_pftreestate ts.top_goal in 
@@ -131,7 +131,7 @@ let restart_proof () =
   match Edit.read proof_edits with
     | None -> 
 	errorlabstrm "Pfedit.restart"
-          [< 'sTR"No focused proof to restart" ; msg_proofs true >]
+          (str"No focused proof to restart" ++ msg_proofs true)
     | Some(na,_,ts) -> 
 	delete_proof na;
         start (na,ts);
@@ -166,7 +166,7 @@ let undo n =
        subtree - this solution only works properly if undoing one step *)
     if subtree_solved() then  Edit.undo proof_edits 1
   with (Invalid_argument "Edit.undo") ->
-    errorlabstrm "Pfedit.undo" [< 'sTR"No focused proof"; msg_proofs true >]
+    errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
 
 (*********************************************************************)
 (*                  Proof cooking                                    *)
@@ -193,8 +193,8 @@ let refining () = [] <> (Edit.dom proof_edits)
 let check_no_pending_proofs () =
   if refining () then 
     errorlabstrm "check_no_pending_proofs"
-      [< 'sTR"Proof editing in progress" ; (msg_proofs false) ;
-         'sTR"Use \"Abort All\" first or complete proof(s)." >]
+      (str"Proof editing in progress" ++ (msg_proofs false) ++
+         str"Use \"Abort All\" first or complete proof(s).")
 
 let delete_current_proof () = delete_proof (get_current_proof_name ())
 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index af106b1c4b..8e2a9b0eaf 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -116,36 +116,36 @@ let pr_goal g =
   let env = evar_env g in
   let penv = pr_context_of env in
   let pc = prterm_env_at_top env g.evar_concl in
-  [< 'sTR"  "; hV 0 [< penv; 'fNL;
-		       'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
-                       'sTR "============================"; 'fNL ;
-                       'sTR" " ; pc>]; 'fNL>]
+  str"  " ++ hv 0 (penv ++ fnl () ++
+		   str (emacs_str (String.make 1 (Char.chr 253)))  ++
+                   str "============================" ++ fnl ()  ++
+                   str" "  ++ pc) ++ fnl ()
 
 let pr_concl n g =
   let env = evar_env g in
   let pc = prterm_env_at_top env g.evar_concl in
-  [< 'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
-     'sTR "subgoal ";'iNT n;'sTR " is:";'cUT;'sTR" " ; pc >]
+  str (emacs_str (String.make 1 (Char.chr 253)))  ++
+  str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
 
 (* print the subgoals but write Subtree proved! even in case some existential 
    variables remain unsolved, pr_subgoals_existential is a safer version 
    of pr_subgoals *)
 
 let pr_subgoals = function
-  | [] -> [< 'sTR"Subtree proved!" ; 'fNL >]
+  | [] -> (str"Subtree proved!" ++ fnl ())
   | [g] ->
-      let pg = pr_goal g in v 0 [< 'sTR ("1 "^"subgoal");'cUT; pg >]
+      let pg = pr_goal g in v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
   | g1::rest ->
       let rec pr_rec n = function
-        | [] -> [< >]
+        | [] -> (mt ())
         | g::rest ->
             let pg = pr_concl n g in
             let prest = pr_rec (n+1) rest in
-            [< 'cUT; pg; prest >] 
+            (cut () ++ pg ++ prest) 
       in
       let pg1 = pr_goal g1 in
       let pgr = pr_rec 2 rest in
-      v 0 [< 'iNT(List.length rest+1) ; 'sTR" subgoals" ;'cUT; pg1; pgr >]
+      v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () ++ pg1 ++ pgr)
 
 let pr_subgoal n =
   let rec prrec p = function
@@ -153,7 +153,7 @@ let pr_subgoal n =
     | g::rest ->
        	if p = 1 then
           let pg = pr_goal g in
-          v 0 [< 'sTR "subgoal ";'iNT n;'sTR " is:"; 'cUT; pg >]
+          v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg)
        	else 
 	  prrec (p-1) rest
   in 
@@ -165,85 +165,85 @@ let pr_seq evd =
   in
   let pdcl = pr_named_context_of env in
   let pcl = prterm_env_at_top env cl in
-  hOV 0 [< pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >]
+  hov 0 (pdcl  ++ spc ()  ++ hov 0 (str"|- "  ++ pcl))
 
 let prgl gl =
   let pgl = pr_seq gl in
-  [< 'sTR"[" ; pgl ; 'sTR"]" ; 'sPC >]
+  (str"["  ++ pgl  ++ str"]"  ++ spc ())
 
 let pr_evgl gl =
   let phyps = pr_idl (ids_of_named_context gl.evar_hyps) in
   let pc = prterm gl.evar_concl in
-  hOV 0 [< 'sTR"[" ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
+  hov 0 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pc ++ str"]")
 
 let pr_evgl_sign gl = 
   let ps = pr_named_context_of (evar_env gl) in
   let pc = prterm gl.evar_concl in
-  hOV 0 [< 'sTR"[" ; ps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
+  hov 0 (str"["  ++ ps ++ spc () ++ str"|- "  ++ pc ++ str"]")
 
 (*  evd.evgoal.lc seems to be printed twice *)
 let pr_decl evd =
   let pevgl = pr_evgl evd in
   let pb =
     match evd.evar_body with
-      | Evar_empty -> [< 'fNL >]
-      | Evar_defined c -> let pc = prterm c in [< 'sTR" => " ; pc;  'fNL  >]
+      | Evar_empty -> (fnl ())
+      | Evar_defined c -> let pc = prterm c in (str" => "  ++ pc ++  fnl ())
   in
-  h 0 [< pevgl; pb >]
+  h 0 (pevgl ++ pb)
 
 let pr_evd evd = 
   prlist_with_sep pr_fnl
     (fun (ev,evd) ->
        let pe = pr_decl evd in 
-       h 0 [< pr_id (id_of_existential ev) ; 'sTR"==" ; pe >])
+       h 0 (pr_id (id_of_existential ev)  ++ str"=="  ++ pe))
     (Evd.to_list evd)
     
 let pr_decls decls = pr_evd decls
 		       
 let pr_evc evc =
   let pe = pr_evd evc.sigma in
-  [< pe >]
+  (pe)
 
 let pr_evars = 
   prlist_with_sep pr_fnl
     (fun (ev,evd) ->
        let pegl = pr_evgl_sign evd in 
-       [< pr_id (id_of_existential ev); 'sTR " : "; pegl >])
+       (pr_id (id_of_existential ev) ++ str " : " ++ pegl))
 
 (* Print an enumerated list of existential variables *)
 let rec pr_evars_int i = function
-  | [] -> [< >]
+  | [] -> (mt ())
   | (ev,evd)::rest ->
       let pegl = pr_evgl_sign evd in 
       let pei = pr_evars_int (i+1) rest in
-      [< (hOV 0 [< 'sTR "Existential "; 'iNT i; 'sTR " ="; 'sPC;
-                   pr_id (id_of_existential ev) ; 'sTR " : "; pegl >]); 
-	 'fNL ; pei >]
+      (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
+              pr_id (id_of_existential ev)  ++ str " : " ++ pegl)) ++ 
+      fnl () ++ pei
 
 let pr_subgoals_existential sigma = function 
   | [] -> 
       let exl = Evd.non_instantiated sigma in 
       if exl = [] then 
-	[< 'sTR"Subtree proved!" ; 'fNL >]
+	(str"Subtree proved!"  ++ fnl ())
       else
         let pei = pr_evars_int 1 exl in
-        [< 'sTR "No more subgoals but non-instantiated existential ";
-           'sTR "variables :" ;'fNL; (hOV 0 pei) >]
+        (str "No more subgoals but non-instantiated existential " ++
+           str "variables :"  ++fnl () ++ (hov 0 pei))
   | [g] ->
       let pg = pr_goal g in
-      v 0 [< 'sTR ("1 "^"subgoal");'cUT; pg >]
+      v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
   | g1::rest ->
       let rec pr_rec n = function
-        | [] -> [< >]
+        | [] -> (mt ())
         | g::rest ->
             let pc = pr_concl n g in
             let prest = pr_rec (n+1) rest in
-            [< 'cUT; pc; prest >] 
+            (cut () ++ pc ++ prest) 
       in
       let pg1 = pr_goal g1 in
       let prest = pr_rec 2 rest in
-      v 0 [< 'iNT(List.length rest+1) ; 'sTR" subgoals" ;'cUT; pg1; prest;
-             'fNL >]
+      v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () 
+	   ++ pg1 ++ prest ++ fnl ())
 
 open Ast
 open Termast
@@ -308,7 +308,7 @@ let ast_of_cvt_redexp = function
 let ast_of_cvt_arg = function
   | Identifier id   -> nvar id
   | Qualid qid      -> ast_of_qualid qid
-  | Quoted_string s -> str s
+  | Quoted_string s -> string s
   | Integer n       -> num n 
   | Command c       -> ope ("COMMAND",[c])
   | Constr  c       -> 
@@ -316,8 +316,8 @@ let ast_of_cvt_arg = function
   | OpenConstr  (_,c)       -> 
     ope ("COMMAND",[ast_of_constr false (Global.env ()) c])
   | Constr_context _ ->
-    anomalylabstrm "ast_of_cvt_arg" [<'sTR
-      "Constr_context argument could not be used">]
+    anomalylabstrm "ast_of_cvt_arg" (str
+      "Constr_context argument could not be used")
   | Clause idl      -> 
       let transl = function
 	| InHyp id -> ope ("INHYP", [nvar id])
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a645cf0f04..6806cf2b6b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -91,7 +91,7 @@ let rec frontier p =
 	      p'
             else 
 	      errorlabstrm "Refiner.frontier"
-                [< 'sTR"frontier was handed back a ill-formed proof." >]))
+                (str"frontier was handed back a ill-formed proof.")))
     | Some(r,pfl) ->
     	let gll,vl = List.split(List.map frontier pfl) in
     	(List.flatten gll,
@@ -131,7 +131,7 @@ let tac_tab = Hashtbl.create 17
 let add_tactic s t =
   if Hashtbl.mem tac_tab s then
     errorlabstrm ("Refiner.add_tactic: "^s) 
-      [<'sTR "Cannot redeclare a tactic.">];
+      (str "Cannot redeclare a tactic.");
   Hashtbl.add tac_tab s t
 
 let overwriting_add_tactic s t =
@@ -146,13 +146,13 @@ let lookup_tactic s =
     Hashtbl.find tac_tab s
   with Not_found -> 
     errorlabstrm "Refiner.lookup_tactic"
-      [< 'sTR"The tactic " ; 'sTR s ; 'sTR" is not installed" >]
+      (str"The tactic " ++ str s ++ str" is not installed")
 
 
 (* refiner r is a tactic applying the rule r *)
 
 let bad_subproof () =
-  anomalylabstrm "Refiner.refiner" [< 'sTR"Bad subproof in validation.">]
+  anomalylabstrm "Refiner.refiner" (str"Bad subproof in validation.")
 
 let check_subproof_connection gl spfl =
   if not (list_for_all2eq (fun g pf -> g=pf.goal) gl spfl)
@@ -290,7 +290,7 @@ let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma}
 let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
 
 (* General failure tactic *)
-let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" [< 'sTR s>]
+let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
 
 (* A special exception for levels for the Fail tactic *)
 exception FailError of int
@@ -308,7 +308,7 @@ let thens_tac tac2l taci (sigr,gs,p) =
   let (gl,gi) =
     try list_chop (List.length tac2l) gs
     with Failure _ -> errorlabstrm "Refiner.combine_tactics"
-        [<'sTR "Wrong number of tactics.">] in
+        (str "Wrong number of tactics.") in
   let tac2gl =
     List.combine gl tac2l @ list_map_i (fun i g -> (g, taci i)) 1 gi in
   let gll,pl =
@@ -321,14 +321,14 @@ let then_tac tac = thens_tac [] (fun _ -> tac)
 
 let non_existent_goal n =
   errorlabstrm ("No such goal: "^(string_of_int n))
-    [< 'sTR"Trying to apply a tactic to a non existent goal" >]
+    (str"Trying to apply a tactic to a non existent goal")
 
 (* Apply tac on the i-th goal (if i>0). If i<0, then start counting from
    the last goal (i=-1). *)
 let theni_tac i tac ((_,gl,_) as subgoals) =
   let nsg = List.length gl in
   let k = if i < 0 then nsg + i + 1 else i in
-  if nsg < 1 then errorlabstrm "theni_tac" [< 'sTR"No more subgoals.">]
+  if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.")
   else if k >= 1 & k <= nsg then
     thens_tac [] (fun i -> if i = k then tac else tclIDTAC) subgoals
   else non_existent_goal k 
@@ -398,14 +398,14 @@ the goal unchanged *)
 let tclPROGRESS tac ptree =
   let rslt = tac ptree in
   if progress (fst rslt) ptree then rslt
-  else errorlabstrm "Refiner.PROGRESS" [< 'sTR"Failed to progress.">]
+  else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.")
 
 (* weak_PROGRESS tac ptree applies tac to the goal ptree and fails 
    if tac leaves the goal unchanged, possibly modifying sigma *)
 let tclWEAK_PROGRESS tac ptree =
   let rslt = tac ptree in
   if weak_progress (fst rslt) ptree then rslt
-  else errorlabstrm "Refiner.tclWEAK_PROGRESS" [< 'sTR"Failed to progress.">]
+  else errorlabstrm "Refiner.tclWEAK_PROGRESS" (str"Failed to progress.")
 
 
 (* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
@@ -415,7 +415,7 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
   let gls = (fst rslt).it in
   if List.exists (same_goal goal.it) gls
   then errorlabstrm "Refiner.tclNOTSAMEGOAL" 
-      [< 'sTR"Tactic generated a subgoal identical to the original goal.">]
+      (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
 
 
@@ -461,7 +461,7 @@ let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
 let tclDO n t = 
   let rec dorec k = 
     if k < 0 then errorlabstrm "Refiner.tclDO"
-      [<'sTR"Wrong argument : Do needs a positive integer.">];
+      (str"Wrong argument : Do needs a positive integer.");
     if k = 0 then tclIDTAC
     else if k = 1 then t else (tclTHEN t (dorec (k-1)))
   in 
@@ -660,12 +660,12 @@ let extract_open_pftreestate pts =
 let extract_pftreestate pts =
   if pts.tstack <> [] then
     errorlabstrm "extract_pftreestate"
-      [< 'sTR"Cannot extract from a proof-tree in which we have descended;" ;
-         'sPC; 'sTR"Please ascend to the root" >];
+      (str"Cannot extract from a proof-tree in which we have descended;" ++
+         spc () ++ str"Please ascend to the root");
   let pfterm,subgoals = extract_open_pftreestate pts in
   if subgoals <> [] then
    errorlabstrm "extract_proof"
-   [< 'sTR "Attempt to save an incomplete proof" >];
+   (str "Attempt to save an incomplete proof");
   let env = Global.env_of_context pts.tpf.goal.evar_hyps in
   strong whd_betaiotaevar env pts.tpfsigma pfterm
   (***
@@ -676,7 +676,7 @@ let extract_pftreestate pts =
 let rec first_unproven pts =
   let pf = (proof_of_pftreestate pts) in 
   if is_complete_proof pf then
-    errorlabstrm "first_unproven" [< 'sTR"No unproven subgoals" >];
+    errorlabstrm "first_unproven" (str"No unproven subgoals");
   if is_leaf_proof pf then
     pts
   else
@@ -693,7 +693,7 @@ let rec first_unproven pts =
 let rec last_unproven pts =
   let pf = proof_of_pftreestate pts in 
   if is_complete_proof pf then
-    errorlabstrm "last_unproven" [< 'sTR"No unproven subgoals" >];
+    errorlabstrm "last_unproven" (str"No unproven subgoals");
   if is_leaf_proof pf then
     pts
   else 
@@ -710,17 +710,17 @@ let rec last_unproven pts =
 let rec nth_unproven n pts =
   let pf = proof_of_pftreestate pts in 
   if is_complete_proof pf then
-    errorlabstrm "nth_unproven" [< 'sTR"No unproven subgoals" >];
+    errorlabstrm "nth_unproven" (str"No unproven subgoals");
   if is_leaf_proof pf then
     if n = 1 then 
       pts 
     else
-      errorlabstrm "nth_unproven" [< 'sTR"Not enough unproven subgoals" >]
+      errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
   else 
     let children = children_of_proof pf in
     let rec process i k = function
       | [] -> 
-	  errorlabstrm "nth_unproven" [< 'sTR"Not enough unproven subgoals" >]
+	  errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
       | pf1::rest -> 
 	  let k1 = nb_unsolved_goals pf1 in 
 	  if k1 < k then 
@@ -789,17 +789,17 @@ let pr_tactic (s,l) =
 
 let pr_rule = function
   | Prim r -> pr_prim_rule r
-  | Tactic texp -> hOV 0 (pr_tactic texp)
+  | Tactic texp -> hov 0 (pr_tactic texp)
   | Change_evars ->
       (* This is internal tactic and cannot be replayed at user-level.
          Function pr_rule_dot below is used when we want to hide
          Change_evars *)
-       [< 'sTR"Evar change" >]
+      str "Evar change"
 
 (* Does not print change of evars *)
 let pr_rule_dot = function 
-  | Change_evars -> [<>]
-  | r -> [< pr_rule r; 'sTR"." ; 'fNL >] 
+  | Change_evars -> (mt ())
+  | r -> (pr_rule r ++ str"." ++ fnl ()) 
 
 exception Different
 
@@ -819,69 +819,68 @@ let rec print_proof sigma osign pf =
   let hyps' = thin_sign osign hyps in
   match pf.ref with
     | None -> 
-	hOV 0 [< pr_seq {evar_hyps=hyps'; evar_concl=cl;
-			 evar_body=body} >]
+	hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body})
     | Some(r,spfl) ->
-    	hOV 0 [< hOV 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl;
-				evar_body=body});
-		 'sPC ; 'sTR" BY ";
-		 hOV 0 [< pr_rule r >]; 'fNL ;
-		 'sTR"  ";
-		 hOV 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)
-              >]
+    	hov 0 
+	  (hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++
+	   spc () ++ str" BY " ++
+	   hov 0 (pr_rule r) ++ fnl () ++
+	   str"  " ++
+	   hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)
+)
 	  
-let pr_change gl = [< 'sTR"Change " ; prterm gl.evar_concl ; 'sTR"." ; 'fNL>]
+let pr_change gl = (str"Change " ++ prterm gl.evar_concl ++ str"." ++ fnl ())
 		     
 let rec print_script nochange sigma osign pf =
   let {evar_hyps=sign; evar_concl=cl} = pf.goal in
   match pf.ref with
     | None ->
         if nochange then 
-	  [< 'sTR"<Your Tactic Text here>" >] 
+	  (str"<Your Tactic Text here>") 
 	else 
 	  pr_change pf.goal
     | Some(r,spfl) ->
-        [< (if nochange then [< >] else (pr_change pf.goal));
-           pr_rule_dot r;
+        ((if nochange then (mt ()) else (pr_change pf.goal)) ++
+           pr_rule_dot r ++
            prlist_with_sep pr_fnl
-             (print_script nochange sigma sign) spfl >]
+             (print_script nochange sigma sign) spfl)
 
 let rec print_treescript sigma osign pf =
   let {evar_hyps=sign; evar_concl=cl} = pf.goal in
   match pf.ref with
-    | None -> [< >]
+    | None -> (mt ())
     | Some(r,spfl) ->
-        [< pr_rule_dot r ;
+        (pr_rule_dot r ++
            let prsub =
              prlist_with_sep pr_fnl (print_treescript sigma sign) spfl
            in
            if List.length spfl > 1 then 
-	     [< 'sTR"  "; hOV 0 prsub >]
+	     (str"  " ++ hov 0 prsub)
            else 
 	     prsub 
-	>]
+)
 
 let rec print_info_script sigma osign pf =
   let {evar_hyps=sign; evar_concl=cl} = pf.goal in
   match pf.ref with
-    | None -> [< >]
+    | None -> (mt ())
     | Some(Change_evars,[spf]) ->
         print_info_script sigma osign spf
     | Some(r,spfl) ->
-        [< pr_rule r ; 
+        (pr_rule r ++ 
            match spfl with
              | [pf1] ->
                  if pf1.ref = None then 
-		   [<'sTR "."; 'fNL >]
+		   (str "." ++ fnl ())
                  else 
-		   [< 'sTR";" ; 'bRK(1,3) ;
-		      print_info_script sigma sign pf1 >]
-             | _ -> [< 'sTR"." ; 'fNL ;
+		   (str";" ++ brk(1,3) ++
+		      print_info_script sigma sign pf1)
+             | _ -> (str"." ++ fnl () ++
                        prlist_with_sep pr_fnl
-                         (print_info_script sigma sign) spfl >] >]
+                         (print_info_script sigma sign) spfl))
 
 let format_print_info_script sigma osign pf = 
-  hOV 0 (print_info_script sigma osign pf)
+  hov 0 (print_info_script sigma osign pf)
     
 let print_subscript sigma sign pf = 
   if is_tactic_proof pf then 
@@ -894,10 +893,9 @@ let tclINFO (tac : tactic) gls =
   begin try 
     let pf = v (List.map leaf (sig_it sgl)) in
     let sign = (sig_it gls).evar_hyps in
-    mSGNL(hOV 0 [< 'sTR" == "; 
-                   print_subscript 
-                     (sig_sig gls) sign pf >])
+    msgnl (hov 0 (str" == " ++
+                  print_subscript (sig_sig gls) sign pf))
   with e when catchable_exception e -> 
-    mSGNL(hOV 0 [< 'sTR "Info failed to apply validation" >])
+    msgnl (hov 0 (str "Info failed to apply validation"))
   end;
   res
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 56fe36890a..08535e6415 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -37,7 +37,7 @@ open Safe_typing
 let err_msg_tactic_not_found macro_loc macro =
   user_err_loc
     (macro_loc,"macro_expand",
-     [<'sTR "Tactic macro "; 'sTR macro; 'sPC; 'sTR "not found">])
+     (str "Tactic macro " ++ str macro ++ spc () ++ str "not found"))
 
 (* Values for interpretation *)
 type value =
@@ -74,24 +74,24 @@ let tactic_of_value vle g =
 let id_of_Identifier = function
   | Identifier id -> id
   | _ ->
-    anomalylabstrm "id_of_Identifier" [<'sTR "Not an IDENTIFIER tactic_arg">]
+    anomalylabstrm "id_of_Identifier" (str "Not an IDENTIFIER tactic_arg")
 
 (* Gives the constr corresponding to a Constr tactic_arg *)
 let constr_of_Constr = function
   | Constr c -> c
-  | _ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a Constr tactic_arg">]
+  | _ -> anomalylabstrm "constr_of_Constr" (str "Not a Constr tactic_arg")
 
 (* Gives the constr corresponding to a Constr_context tactic_arg *)
 let constr_of_Constr_context = function
   | Constr_context c -> c
   | _ ->
-    anomalylabstrm "constr_of_Constr_context" [<'sTR
-      "Not a Constr_context tactic_arg">]
+    anomalylabstrm "constr_of_Constr_context" (str
+      "Not a Constr_context tactic_arg")
 
 (* Gives the qualid corresponding to a Qualid tactic_arg *)
 let qualid_of_Qualid = function
   | Qualid id -> id
-  | _ -> anomalylabstrm "qualid_of_Qualid" [<'sTR "Not a Qualid tactic_arg">]
+  | _ -> anomalylabstrm "qualid_of_Qualid" (str "Not a Qualid tactic_arg")
 
 (* Gives identifiers and makes the possible injection constr -> ident *)
 let make_ids ast = function
@@ -100,9 +100,9 @@ let make_ids ast = function
     (try destVar c with
     | Invalid_argument "destVar" ->
       anomalylabstrm "make_ids"
-      [<'sTR "This term cannot be reduced to an identifier"; 'fNL;
-        print_ast ast>])
-  | _ -> anomalylabstrm "make_ids" [< 'sTR "Not an identifier" >]
+      (str "This term cannot be reduced to an identifier" ++ fnl () ++
+        print_ast ast))
+  | _ -> anomalylabstrm "make_ids" (str "Not an identifier")
 
 (* Gives Qualid's and makes the possible injection identifier -> qualid *)
 let make_qid = function
@@ -111,8 +111,8 @@ let make_qid = function
   | VArg (Constr c) ->
     (match (kind_of_term c) with
     | Const cst -> VArg (Qualid (qualid_of_sp cst))
-    | _ -> anomalylabstrm "make_qid" [< 'sTR "Not a Qualid" >])
-  | _ -> anomalylabstrm "make_qid" [< 'sTR "Not a Qualid" >]
+    | _ -> anomalylabstrm "make_qid" (str "Not a Qualid"))
+  | _ -> anomalylabstrm "make_qid" (str "Not a Qualid")
 
 (* Transforms a named_context into a (string * constr) list *)
 let make_hyps = List.map (fun (id,_,typ) -> (string_of_id id,body_of_type typ))
@@ -160,10 +160,10 @@ let tacticOut = function
     if (tag d) = "tactic" then
       tactic_out d
     else
-      anomalylabstrm "tacticOut" [<'sTR "Dynamic tag should be tactic">]
+      anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic")
   | ast ->
     anomalylabstrm "tacticOut"
-      [<'sTR "Not a Dynamic ast: "; print_ast ast>]
+      (str "Not a Dynamic ast: " ++ print_ast ast)
 
 let valueIn t = Dynamic (dummy_loc,value_in t)
 let valueOut = function
@@ -171,10 +171,10 @@ let valueOut = function
     if (tag d) = "value" then
       value_out d
     else
-      anomalylabstrm "valueOut" [<'sTR "Dynamic tag should be value">]
+      anomalylabstrm "valueOut" (str "Dynamic tag should be value")
   | ast ->
     anomalylabstrm "valueOut"
-      [<'sTR "Not a Dynamic ast: "; print_ast ast>]
+      (str "Not a Dynamic ast: " ++ print_ast ast)
 
 let constrIn = constrIn
 let constrOut = constrOut
@@ -192,8 +192,8 @@ let interp_add (ast_typ,interp_fun) =
   with
       Failure _ ->
         errorlabstrm "interp_add"
-          [<'sTR "Cannot add the interpretation function for "; 'sTR ast_typ;
-            'sTR " twice">]
+          (str "Cannot add the interpretation function for " ++ str ast_typ ++
+            str " twice")
 
 (* Adds a possible existing interpretation function *)
 let overwriting_interp_add (ast_typ,interp_fun) =
@@ -249,7 +249,7 @@ let _ =
 (* Unboxes the tactic_arg *)
 let unvarg = function
   | VArg a -> a
-  | _ -> errorlabstrm "unvarg" [<'sTR "Not a tactic argument">]
+  | _ -> errorlabstrm "unvarg" (str "Not a tactic argument")
 
 (* Unboxes VRec *)
 let unrec = function
@@ -259,7 +259,7 @@ let unrec = function
 (* Unboxes REDEXP *)
 let unredexp = function
   | Redexp c -> c
-  | _ ->  errorlabstrm "unredexp" [<'sTR "Not a REDEXP tactic_arg">]
+  | _ ->  errorlabstrm "unredexp" (str "Not a REDEXP tactic_arg")
 
 (* Reads the head of Fun *)
 let read_fun ast =
@@ -268,12 +268,12 @@ let read_fun ast =
     | Nvar(_,s)::tl -> (Some s)::(read_fun_rec tl)
     | [] -> []
     | _ ->
-      anomalylabstrm "Tacinterp.read_fun_rec" [<'sTR "Fun not well formed">]
+      anomalylabstrm "Tacinterp.read_fun_rec" (str "Fun not well formed")
   in
     match ast with
       | Node(_,"FUNVAR",l) -> read_fun_rec l
       | _ ->
-        anomalylabstrm "Tacinterp.read_fun" [<'sTR "Fun not well formed">]
+        anomalylabstrm "Tacinterp.read_fun" (str "Fun not well formed")
 
 (* Reads the clauses of a Rec *)
 let rec read_rec_clauses = function
@@ -282,7 +282,7 @@ let rec read_rec_clauses = function
     (name,it,body)::(read_rec_clauses tl)
   |_ ->
     anomalylabstrm "Tacinterp.read_rec_clauses"
-      [<'sTR "Rec not well formed">]
+      (str "Rec not well formed")
 
 (* Associates variables with values and gives the remaining variables and
    values *)
@@ -322,8 +322,8 @@ let give_context ctxt = function
 let ast_of_command = function
   | Node(_,"COMMAND",[c]) -> c
   | ast ->
-    anomaly_loc (Ast.loc ast, "Tacinterp.ast_of_command",[<'sTR
-      "Not a COMMAND ast node: "; print_ast ast>])
+    anomaly_loc (Ast.loc ast, "Tacinterp.ast_of_command",(str
+      "Not a COMMAND ast node: " ++ print_ast ast))
 
 (* Reads a pattern *)
 let read_pattern evc env lfun = function
@@ -336,8 +336,8 @@ let read_pattern evc env lfun = function
   | Node(_,"TERM",[pc]) ->
     Term (snd (interp_constrpattern_gen evc env lfun (ast_of_command pc)))
   | ast ->
-    anomaly_loc (Ast.loc ast, "Tacinterp.read_pattern",[<'sTR
-      "Not a pattern ast node: "; print_ast ast>])
+    anomaly_loc (Ast.loc ast, "Tacinterp.read_pattern",(str
+      "Not a pattern ast node: " ++ print_ast ast))
 
 (* Reads the hypotheses of a Match Context rule *)
 let rec read_match_context_hyps evc env lfun = function
@@ -348,8 +348,8 @@ let rec read_match_context_hyps evc env lfun = function
     (Hyp (s,read_pattern evc env lfun mp))::(read_match_context_hyps evc env
       lfun tl)
   | ast::tl ->
-    anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_hyp",[<'sTR
-      "Not a MATCHCONTEXTHYP ast node: "; print_ast ast>])
+    anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_hyp",(str
+      "Not a MATCHCONTEXTHYP ast node: " ++ print_ast ast))
   | [] -> []
 
 (* Reads the rules of a Match Context *)
@@ -362,8 +362,8 @@ let rec read_match_context_rule evc env lfun = function
         rl))),read_pattern evc env lfun (List.nth rl 1),List.hd
         rl))::(read_match_context_rule evc env lfun tl)
   | ast::tl ->
-    anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR
-      "Not a MATCHCONTEXTRULE ast node: "; print_ast ast>])
+    anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",(str
+      "Not a MATCHCONTEXTRULE ast node: " ++ print_ast ast))
   | [] -> []
 
 (* Reads the rules of a Match *)
@@ -374,8 +374,8 @@ let rec read_match_rule evc env lfun = function
     (Pat ([],read_pattern evc env lfun mp,te))::(read_match_rule evc env lfun
       tl)
   | ast::tl ->
-    anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR
-      "Not a MATCHRULE ast node: "; print_ast ast>])
+    anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",(str
+      "Not a MATCHRULE ast node: " ++ print_ast ast))
   | [] -> []
 
 (* For Match Context and Match *)
@@ -472,8 +472,8 @@ let get_debug () = !debug
 (* Interprets any expression *)
 let rec val_interp ist ast =
 
-(* mSGNL [<print_ast ast>]; *)
-(* mSGNL [<print_ast (Termast.ast_of_constr false (Pretty.assumptions_for_print []) c)>] *)
+(* mSGNL (print_ast ast); *)
+(* mSGNL (print_ast (Termast.ast_of_constr false (Pretty.assumptions_for_print []) c)) *)
 
   let value_interp ist =
   match ast with
@@ -574,10 +574,10 @@ let rec val_interp ist ast =
         VArg (Constr (Pretyping.constr_out t))
       else
         anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",
-          [<'sTR "Unknown dynamic ast: "; print_ast ast>])
+          (str "Unknown dynamic ast: " ++ print_ast ast))
     | _ ->
         anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",
-          [<'sTR "Unrecognizable ast: "; print_ast ast>]) in
+          (str "Unrecognizable ast: " ++ print_ast ast)) in
   if ist.debug = DebugOn then
     match debug_prompt ist.goalopt ast with
     | Exit -> VTactic tclIDTAC
@@ -601,7 +601,7 @@ and app_interp ist fv largs ast =
         VFun(olfun@newlfun,lvar,body)
     | _ ->
       user_err_loc (Ast.loc ast, "Tacinterp.app_interp",
-                    [<'sTR"Illegal tactic application: "; print_ast ast>])
+                    (str"Illegal tactic application: " ++ print_ast ast))
 
 (* Interprets recursive expressions *)
 and rec_interp ist ast = function
@@ -626,7 +626,7 @@ and rec_interp ist ast = function
     end
   | _ ->
     anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",
-                 [<'sTR"Rec not well formed: "; print_ast ast>])
+                 (str"Rec not well formed: " ++ print_ast ast))
 
 (* Interprets the clauses of a Let *)
 and let_interp ist ast = function
@@ -635,7 +635,7 @@ and let_interp ist ast = function
       (id,val_interp ist t)::(let_interp ist ast tl)
   | _ ->
       anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",
-                   [<'sTR"Let not well formed: "; print_ast ast>])
+                   (str"Let not well formed: " ++ print_ast ast))
 
 (* Interprets the clauses of a LetCutIn *)
 and letin_interp ist ast = function
@@ -654,7 +654,7 @@ and letin_interp ist ast = function
          (letin_interp ist ast tl)
        with | Not_found ->
          errorlabstrm "Tacinterp.letin_interp"
-         [< 'sTR "Term or tactic expected" >])
+         (str "Term or tactic expected"))
     | _ ->
       (try
          let t = tactic_of_value tac in
@@ -671,10 +671,10 @@ and letin_interp ist ast = function
        with | NotTactic ->
          delete_proof id;
          errorlabstrm "Tacinterp.letin_interp"
-         [< 'sTR "Term or tactic expected" >]))
+         (str "Term or tactic expected")))
   | _ ->
     anomaly_loc (Ast.loc ast, "Tacinterp.letin_interp",
-    [<'sTR "LetIn not well formed: "; print_ast ast>])
+    (str "LetIn not well formed: " ++ print_ast ast))
 
 (* Interprets the clauses of a LetCut *)
 and letcut_interp ist ast = function
@@ -685,8 +685,8 @@ and letcut_interp ist ast = function
     and (ndc,ccl) =
       match ist.goalopt with
       |	None -> 
-        errorlabstrm "Tacinterp.letcut_interp" [< 'sTR
-        "Do not use Let for toplevel definitions, use Lemma, ... instead" >]
+        errorlabstrm "Tacinterp.letcut_interp" (str
+        "Do not use Let for toplevel definitions, use Lemma, ... instead")
       |	Some g -> (pf_hyps g,pf_concl g) in
     (match tac with
     | VArg (Constr csr) ->
@@ -709,7 +709,7 @@ and letcut_interp ist ast = function
          (letcut_interp ist ast tl);exat]
        with | Not_found ->
          errorlabstrm "Tacinterp.letin_interp"
-         [< 'sTR "Term or tactic expected" >])
+         (str "Term or tactic expected"))
     | _ ->
       (try
          let t = tactic_of_value tac in
@@ -730,18 +730,18 @@ and letcut_interp ist ast = function
        with | NotTactic ->
          delete_proof id;
          errorlabstrm "Tacinterp.letcut_interp"
-         [< 'sTR "Term or tactic expected" >]))
+         (str "Term or tactic expected")))
   | _ ->
-    anomaly_loc (Ast.loc ast, "Tacinterp.letcut_interp",[<'sTR
-      "LetCut not well formed: "; print_ast ast>])
+    anomaly_loc (Ast.loc ast, "Tacinterp.letcut_interp",(str
+      "LetCut not well formed: " ++ print_ast ast))
 
 (* Interprets the Match Context expressions *)
 and match_context_interp ist ast lmr =
 (*  let goal =
     (match goalopt with
     | None ->
-      errorlabstrm "Tacinterp.apply_match_context" [< 'sTR
-        "No goal available" >]
+      errorlabstrm "Tacinterp.apply_match_context" (str
+        "No goal available")
     | Some g -> g) in*)
   let rec apply_goal_sub ist goal nocc (id,c)
     csr mt mhyps hyps =
@@ -793,8 +793,8 @@ and match_context_interp ist ast lmr =
          with
         | No_match | _ -> apply_match_context ist goal tl))
     | _ ->
-      errorlabstrm "Tacinterp.apply_match_context" [<'sTR
-        "No matching clauses for Match Context">] in
+      errorlabstrm "Tacinterp.apply_match_context" (str
+        "No matching clauses for Match Context") in
   let app_wo_goal = 
     (fun ist goal ->
        apply_match_context ist goal
@@ -855,8 +855,8 @@ and apply_hyps_context ist mt lgmatch mhyps hyps =
               (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1))))
         end
       |	[] ->
-        anomalylabstrm "apply_hyps_context_rec" [<'sTR
-          "Empty list should not occur" >] in
+        anomalylabstrm "apply_hyps_context_rec" (str
+          "Empty list should not occur") in
   apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None
 
 (* Interprets a VContext value *)
@@ -925,8 +925,8 @@ and match_interp ist ast lmr =
          with | No_match ->
            apply_match ist csr tl))
     | _ ->
-      errorlabstrm "Tacinterp.apply_match" [<'sTR
-        "No matching clauses for Match">] in
+      errorlabstrm "Tacinterp.apply_match" (str
+        "No matching clauses for Match") in
   let csr = constr_of_Constr (unvarg (val_interp ist (List.hd lmr)))
   and ilr = read_match_rule ist.evc ist.env (constr_list ist.goalopt ist.lfun)
     (List.tl lmr) in
@@ -943,19 +943,19 @@ and tac_interp lfun lmatch debug ast g =
               goalopt=Some g; debug=debug } in
   try tactic_of_value (val_interp ist ast) g
   with | NotTactic ->
-    errorlabstrm "Tacinterp.tac_interp" [<'sTR
-      "Must be a command or must give a tactic value">]
+    errorlabstrm "Tacinterp.tac_interp" (str
+      "Must be a command or must give a tactic value")
 
-(*    errorlabstrm "Tacinterp.tac_interp" [<'sTR
-    "Interpretation gives a non-tactic value">] *)
+(*    errorlabstrm "Tacinterp.tac_interp" (str
+    "Interpretation gives a non-tactic value") *)
 
 (*    match (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) with
       | VTactic tac -> (tac g)
       | VFTactic (largs,f) -> (f largs g) 
       | VRTactic res -> res
       | _ ->
-        errorlabstrm "Tacinterp.tac_interp" [<'sTR
-          "Interpretation gives a non-tactic value">]*)
+        errorlabstrm "Tacinterp.tac_interp" (str
+          "Interpretation gives a non-tactic value")*)
 
 (* Interprets a primitive tactic *)
 and interp_atomic opn args = vernac_tactic(opn,args)
@@ -985,8 +985,8 @@ and bind_interp ist = function
       (val_interp ist
       (Node(loc,"COMMAND",[c])))))
   | x ->
-    errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding";
-      print_ast x>]
+    errorlabstrm "bind_interp" (str "Not the expected form in binding" ++
+      print_ast x)
 
 (* Interprets a COMMAND expression (in case of failure, returns Command) *)
 and com_interp ist com = 
@@ -1002,8 +1002,8 @@ and com_interp ist com =
         subst_meta [-1,ic] ctxt
        with
       | Not_found ->
-        errorlabstrm "com_interp" [<'sTR "Unbound context identifier";
-          print_ast ast>])
+        errorlabstrm "com_interp" (str "Unbound context identifier" ++
+          print_ast ast))
     | c -> interp_constr ist c None in
   begin
     db_constr ist.debug ist.env csr;
@@ -1027,14 +1027,14 @@ and cast_com_interp ist com =
           and ctxt = constr_of_Constr_context
             (unvarg (List.assoc s ist.lfun)) in
           begin
-           wARNING [<'sTR
-              "Cannot pre-constrain the context expression with goal">];
+           warning 
+             "Cannot pre-constrain the context expression with goal";
             subst_meta [-1,ic] ctxt
           end
          with
          | Not_found ->
-           errorlabstrm "cast_com_interp" [<'sTR "Unbound context identifier";
-             print_ast ast>])
+           errorlabstrm "cast_com_interp" (str "Unbound context identifier" ++
+             print_ast ast))
       | c ->
         interp_constr ist c (Some (pf_concl gl)) in
     begin
@@ -1042,7 +1042,7 @@ and cast_com_interp ist com =
       VArg (Constr csr)
     end
   | None ->
-    errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">]
+    errorlabstrm "val_interp" (str "Cannot cast a constr without goal")
 
 (* Interprets a CASTEDOPENCOMMAND expression *)
 and cast_opencom_interp ist com =
@@ -1060,19 +1060,19 @@ and cast_opencom_interp ist com =
         and ctxt =
           constr_of_Constr_context (unvarg (List.assoc s ist.lfun)) in
         begin
-          wARNING [<'sTR
-            "Cannot pre-constrain the context expression with goal">];
+          warning 
+            "Cannot pre-constrain the context expression with goal";
           VArg (Constr (subst_meta [-1,ic] ctxt))
         end
        with
       |	Not_found ->
-        errorlabstrm "cast_opencom_interp" [<'sTR "Unbound context identifier";
-          print_ast ast>])
+        errorlabstrm "cast_opencom_interp" (str "Unbound context identifier" ++
+          print_ast ast))
     | c ->
         VArg
 	  (OpenConstr (interp_openconstr ist c (Some (pf_concl gl)))))
   | None ->
-    errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">]
+    errorlabstrm "val_interp" (str "Cannot cast a constr without goal")
 
 (* Interprets a qualified name. This can be a metavariable to be injected *)
 and qid_interp ist = function
@@ -1080,8 +1080,8 @@ and qid_interp ist = function
   | Node(loc,"QUALIDMETA",[Num(_,n)]) ->
       Nametab.qualid_of_sp (destConst(List.assoc n ist.lmatch))
   | ast -> 
-      anomaly_loc (Ast.loc ast, "Tacinterp.qid_interp",[<'sTR
-        "Unrecognizable qualid ast: "; print_ast ast>])
+      anomaly_loc (Ast.loc ast, "Tacinterp.qid_interp",(str
+        "Unrecognizable qualid ast: " ++ print_ast ast))
 
 and cvt_pattern ist = function
   | Node(_,"PATTERN", Node(loc,"COMMAND",[com])::nums) ->
@@ -1136,7 +1136,7 @@ and flag_of_ast ist lf =
     | Node(_,"Zeta",[])::lf -> add_flag (red_add red fZETA) lf
     | Node(loc,("Unf"|"UnfBut"),l)::_ ->
 	user_err_loc(loc,"flag_of_ast",
-                     [<'sTR "Delta must be specified just before">])
+                     (str "Delta must be specified just before"))
 
     | arg::_ -> invalid_arg_loc (Ast.loc arg,"flag_of_ast")
   in
@@ -1167,8 +1167,8 @@ and cvt_intro_pattern ist = function
     ListPat (List.map (cvt_intro_pattern ist) l)
   | x ->
     errorlabstrm "cvt_intro_pattern"
-      [<'sTR "Not the expected form for an introduction pattern!";'fNL;
-        print_ast x>]
+      (str "Not the expected form for an introduction pattern!" ++fnl () ++
+        print_ast x)
 
 (* Interprets a pattern of Let *)
 and cvt_letpattern ist (o,l) = function
@@ -1199,13 +1199,13 @@ let interp = fun ast -> tac_interp [] [] !debug ast
 let hide_interp =
   let htac = hide_tactic "Interp"
     (function [Tacexp t] -> interp t
-     | _ -> anomalylabstrm "hide_interp" [<'sTR "Not a tactic AST">]) in
+     | _ -> anomalylabstrm "hide_interp" (str "Not a tactic AST")) in
   fun ast -> htac [Tacexp ast]
 
 (* For bad tactic calls *)
 let bad_tactic_args s =
   anomalylabstrm s
-    [<'sTR "Tactic "; 'sTR s; 'sTR " called with bad arguments">]
+    (str "Tactic " ++ str s ++ str " called with bad arguments")
 
 (* Declaration of the TAC-DEFINITION object *)
 let (inMD,outMD) =
@@ -1227,9 +1227,9 @@ let add_tacdef na vbody =
   begin
     if Gmap.mem na !mactab then
       errorlabstrm "Tacinterp.add_tacdef" 
-      [< 'sTR
-         "There is already a Meta Definition or a Tactic Definition named ";
-         pr_id na>];
+	(str "There is already a Meta Definition or a Tactic Definition named "
+	 ++
+         pr_id na);
     let _ = Lib.add_leaf na (inMD (na,vbody)) in
-    Options.if_verbose mSGNL [< pr_id na; 'sTR " is defined" >]
+    Options.if_verbose msgnl (pr_id na ++ str " is defined")
   end
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 377893fd27..adb4df3d53 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -482,25 +482,25 @@ let pr_com sigma goal com =
             (Astterm.interp_constr sigma (Evarutil.evar_env goal) com))
 
 let pr_one_binding sigma goal = function
-  | (Dep id,com)  -> [< pr_id id ; 'sTR":=" ; pr_com sigma goal com >]
-  | (NoDep n,com) -> [< 'iNT n ; 'sTR":=" ; pr_com sigma goal com >]
-  | (Com,com)     -> [< pr_com sigma goal com >]
+  | (Dep id,com)  -> pr_id id ++ str ":=" ++ pr_com sigma goal com
+  | (NoDep n,com) -> int n  ++ str ":=" ++ pr_com sigma goal com
+  | (Com,com)     -> pr_com sigma goal com
 
 let pr_bindings sigma goal lb =
   let prf = pr_one_binding sigma goal in
   match lb with 
-    | [] -> [< prlist_with_sep pr_spc prf lb >]
-    | _  -> [<'sTR"with";'sPC;prlist_with_sep pr_spc prf lb >]
+    | [] -> prlist_with_sep pr_spc prf lb
+    | _  -> str "with" ++ spc () ++ prlist_with_sep pr_spc prf lb
 	  
 let rec pr_list f = function
-  | []   -> [<>] 
-  | a::l1 -> [< (f a) ; pr_list f l1>]
+  | []   -> mt ()
+  | a::l1 -> (f a) ++ pr_list f l1
 
 let pr_gls gls =
-  hOV 0 [< pr_decls (sig_sig gls) ; 'fNL ; pr_seq (sig_it gls) >]
+  hov 0 (pr_decls (sig_sig gls) ++ fnl () ++ pr_seq (sig_it gls))
 
 let pr_glls glls =
-  hOV 0 [< pr_decls (sig_sig glls) ; 'fNL ;
-           prlist_with_sep pr_fnl pr_seq (sig_it glls) >]
-
+  hov 0 (pr_decls (sig_sig glls) ++ fnl () ++
+         prlist_with_sep pr_fnl pr_seq (sig_it glls))
+    
 let pr_tactic = Refiner.pr_tactic
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 08446d0112..61ccbcac7c 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -21,26 +21,27 @@ type debug_info =
 
 (* Prints the goal if it exists *)
 let db_pr_goal = function
-  | None -> mSGNL [< 'sTR "No goal" >]
+  | None -> 
+      msgnl (str "No goal")
   | Some g ->
-    mSGNL [<'sTR ("Goal:"); 'fNL; Proof_trees.pr_goal (Tacmach.sig_it g) >]
+      msgnl (str "Goal:" ++ fnl () ++ Proof_trees.pr_goal (Tacmach.sig_it g))
 
 (* Prints the commands *)
 let help () =
-  mSGNL [< 'sTR "Commands: <Enter>=Continue, h=Help, s=Skip, x=Exit" >]
+  msgnl (str "Commands: <Enter>=Continue, h=Help, s=Skip, x=Exit")
 
 (* Prints the state and waits for an instruction *)
 let debug_prompt goalopt tac_ast =
   db_pr_goal goalopt;
-  mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL >];
-(*         'sTR "Commands: <Enter>=Continue, s=Skip, x=Exit" >];*)
-(*  mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL; 'fNL;
-         'sTR "----<Enter>=Continue----s=Skip----x=Exit----" >];*)
+  msg (str "Going to execute:" ++ fnl () ++ (gentacpr tac_ast) ++ fnl ());
+(*         str "Commands: <Enter>=Continue, s=Skip, x=Exit" >];*)
+(*  mSG (str "Going to execute:" ++ fnl () ++ (gentacpr tac_ast) ++ fnl () ++ fnl () ++
+         str "----<Enter>=Continue----s=Skip----x=Exit----");*)
   let rec prompt () =
-    mSG [<'fNL; 'sTR "TcDebug > " >];
+    msg (fnl () ++ str "TcDebug > ");
     flush stdout;
     let inst = read_line () in
-(*    mSGNL [<>];*)
+(*    mSGNL (mt ());*)
     match inst with
     | ""  -> DebugOn
     | "s" -> DebugOff
@@ -56,15 +57,15 @@ let debug_prompt goalopt tac_ast =
 (* Prints a constr *)
 let db_constr debug env c =
   if debug = DebugOn then
-    mSGNL [< 'sTR "Evaluated term --> ";  prterm_env env c >]
+    msgnl (str "Evaluated term --> " ++ prterm_env env c)
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,c) =
   if debug = DebugOn then
-    mSGNL [< 'sTR "Matched hypothesis --> "; 'sTR (id^": ");
-             prterm_env env c >]
+    msgnl (str "Matched hypothesis --> " ++ str (id^": ") ++
+           prterm_env env c)
 
 (* Prints the matched conclusion *)
 let db_matched_concl debug env c =
   if debug = DebugOn then
-    mSGNL [< 'sTR "Matched goal --> "; prterm_env env c >]
+    msgnl (str "Matched goal --> " ++ prterm_env env c)