compat ocaml 3.03

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

13 files changed, 184 insertions, 181 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index a1b251c7af..5c17291088 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -223,8 +223,8 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
         in 
 	if eapply & (nmiss <> 0) then begin
           if verbose then 
-	    wARN [< 'sTR "the hint: EApply "; prterm c;
-		    'sTR " will only be used by EAuto" >]; 
+	    warn (str "the hint: EApply " ++ prterm c ++
+		    str " will only be used by EAuto"); 
           (hd,
            { hname = name;
 	     pri = nb_hyp cty + nmiss;
@@ -249,7 +249,7 @@ let make_resolves env sigma name eap (c,cty) =
       [make_exact_entry; make_apply_entry env sigma eap]
   in 
   if ents = [] then 
-    errorlabstrm "Hint" [< prterm c; 'sPC; 'sTR "cannot be used as a hint" >];
+    errorlabstrm "Hint" (prterm c ++ spc () ++ str "cannot be used as a hint");
   ents
 
 (* used to add an hypothesis to the local hint database *)
@@ -306,7 +306,7 @@ let add_extern name pri (patmetas,pat) tacast dbname =
   match (list_subtract tacmetas patmetas) with
     | i::_ ->
 	errorlabstrm "add_extern" 
-	  [< 'sTR "The meta-variable ?"; 'iNT i; 'sTR" is not bound" >]
+	  (str "The meta-variable ?" ++ int i ++ str" is not bound")
     | []  ->
 	Lib.add_anonymous_leaf
 	  (inAutoHint(dbname, [make_extern name pri pat tacast]))
@@ -479,24 +479,24 @@ let _ =
 (**************************************************************************)
 
 let fmt_autotactic = function
-  | Res_pf (c,clenv) -> [< 'sTR"Apply "; prterm c >]
-  | ERes_pf (c,clenv) -> [< 'sTR"EApply "; prterm c >]
-  | Give_exact c -> [< 'sTR"Exact " ; prterm c >]
+  | Res_pf (c,clenv) -> (str"Apply " ++ prterm c)
+  | ERes_pf (c,clenv) -> (str"EApply " ++ prterm c)
+  | Give_exact c -> (str"Exact " ++ prterm c)
   | Res_pf_THEN_trivial_fail (c,clenv) -> 
-      [< 'sTR"Apply "; prterm c ; 'sTR" ; Trivial" >]
-  | Unfold_nth c -> [< 'sTR"Unfold " ;  pr_global c >]
-  | Extern coqast -> [< 'sTR "Extern "; gentacpr coqast >]
+      (str"Apply " ++ prterm c ++ str" ; Trivial")
+  | Unfold_nth c -> (str"Unfold " ++  pr_global c)
+  | Extern coqast -> (str "Extern " ++ gentacpr coqast)
 
 let fmt_hint v =
-  [< fmt_autotactic v.code; 'sTR"("; 'iNT v.pri; 'sTR")"; 'sPC >]
+  (fmt_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ())
 
 let fmt_hint_list hintlist =
-  [< 'sTR "  "; hOV 0 (prlist fmt_hint hintlist); 'fNL >]
+  (str "  " ++ hov 0 (prlist fmt_hint hintlist) ++ fnl ())
 
 let fmt_hints_db (name,db,hintlist) =
-  [< 'sTR "In the database "; 'sTR name; 'sTR ":";
-     if hintlist = [] then [< 'sTR " nothing"; 'fNL >]
-     else [< 'fNL; fmt_hint_list hintlist >] >]
+  (str "In the database " ++ str name ++ str ":" ++
+     if hintlist = [] then (str " nothing" ++ fnl ())
+     else (fnl () ++ fmt_hint_list hintlist))
 
 (* Print all hints associated to head c in any database *)
 let fmt_hint_list_for_head c = 
@@ -507,16 +507,16 @@ let fmt_hint_list_for_head c =
       dbs 
   in
   if valid_dbs = [] then 
-    [<'sTR "No hint declared for :"; pr_ref_label c >]
+    (str "No hint declared for :" ++ pr_ref_label c)
   else 
-    hOV 0 
-      [< 'sTR"For "; pr_ref_label c; 'sTR" -> "; 'fNL;
-	 hOV 0 (prlist fmt_hints_db valid_dbs) >]
+    hov 0 
+      (str"For " ++ pr_ref_label c ++ str" -> " ++ fnl () ++
+	 hov 0 (prlist fmt_hints_db valid_dbs))
 
 let fmt_hint_ref ref = fmt_hint_list_for_head (label_of_ref ref)
 
 (* Print all hints associated to head id in any database *)
-let print_hint_qid qid =  pPNL(fmt_hint_ref (Nametab.global dummy_loc qid))
+let print_hint_qid qid =  ppnl(fmt_hint_ref (Nametab.global dummy_loc qid))
 
 let fmt_hint_term cl = 
   try 
@@ -538,14 +538,14 @@ let fmt_hint_term cl =
 	  dbs
     in 
     if valid_dbs = [] then 
-      [<'sTR "No hint applicable for current goal" >]
+      (str "No hint applicable for current goal")
     else
-      [< 'sTR "Applicable Hints :"; 'fNL;
-	 hOV 0 (prlist fmt_hints_db valid_dbs) >]
+      (str "Applicable Hints :" ++ fnl () ++
+	 hov 0 (prlist fmt_hints_db valid_dbs))
   with Bound | Match_failure _ | Failure _ -> 
-    [<'sTR "No hint applicable for current goal" >]
+    (str "No hint applicable for current goal")
 	  
-let print_hint_term cl = pPNL (fmt_hint_term cl)
+let print_hint_term cl = ppnl (fmt_hint_term cl)
 
 (* print all hints that apply to the concl of the current goal *)
 let print_applicable_hint () = 
@@ -557,9 +557,9 @@ let print_applicable_hint () =
 let print_hint_db db =
   Hint_db.iter 
     (fun head hintlist ->
-       mSG (hOV 0 
-	      [< 'sTR "For "; pr_ref_label head; 'sTR " -> ";
-		 fmt_hint_list hintlist >]))
+       msg (hov 0 
+	      (str "For " ++ pr_ref_label head ++ str " -> " ++
+		 fmt_hint_list hintlist)))
     db
 
 let print_hint_db_by_name dbname =
@@ -572,7 +572,7 @@ let print_hint_db_by_name dbname =
 let print_searchtable () =
   Stringmap.iter
     (fun name db ->
-       mSG [< 'sTR "In the database "; 'sTR name; 'fNL >];
+       msg (str "In the database " ++ str name ++ fnl ());
        print_hint_db db)
     !searchtable
 
@@ -728,7 +728,7 @@ let decomp_unary_term c gls =
   if Hipattern.is_conjunction hd then 
     simplest_case c gls 
   else 
-    errorlabstrm "Auto.decomp_unary_term" [<'sTR "not a unary type" >] 
+    errorlabstrm "Auto.decomp_unary_term" (str "not a unary type") 
 
 let decomp_empty_term c gls = 
   let typc = pf_type_of gls c in 
@@ -736,7 +736,7 @@ let decomp_empty_term c gls =
   if Hipattern.is_empty_type hd then 
     simplest_case c gls 
   else 
-    errorlabstrm "Auto.decomp_empty_term" [<'sTR "not an empty type" >] 
+    errorlabstrm "Auto.decomp_empty_term" (str "not an empty type") 
 
 
 (* decomp is an natural number giving an indication on decomposition 
@@ -941,20 +941,20 @@ let cvt_autoArg = function
   | "UsingTDB"     -> [UsingTDB]
   | "NoAutoArg"    -> []
   | x -> errorlabstrm "cvt_autoArg"
-        [< 'sTR "Unexpected argument for Auto!"; 'sTR x >]
+        (str "Unexpected argument for Auto!" ++ str x)
 
 let cvt_autoArgs =
   list_join_map
     (function 
        | Quoted_string s -> (cvt_autoArg s)
-       | _ -> errorlabstrm "cvt_autoArgs" [< 'sTR "String expected" >])
+       | _ -> errorlabstrm "cvt_autoArgs" (str "String expected"))
 
 let interp_to_add gl = function
   | Qualid qid ->
       let _,id = Nametab.repr_qualid qid in
       (next_ident_away id (pf_ids_of_hyps gl), 
        Declare.constr_of_reference (Nametab.global dummy_loc qid))
-  | _ -> errorlabstrm "cvt_autoArgs" [< 'sTR "Qualid expected" >]
+  | _ -> errorlabstrm "cvt_autoArgs" (str "Qualid expected")
 
 let dyn_superauto l g = 
   match l with
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c8d1c43703..3216a6065b 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -44,7 +44,7 @@ let one_base tac_main bas =
   let lrul = Hashtbl.find_all !rewtab bas in
   if lrul = [] then
     errorlabstrm "AutoRewrite"
-      [<'sTR ("Rewriting base "^(bas)^" does not exist") >]
+      (str ("Rewriting base "^(bas)^" does not exist"))
   else
     tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
       tclTHEN tac
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 839c639789..10e4230d65 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -77,7 +77,7 @@ hypothesis" is defined in this way:
 
 Require DHyp.
 Hint Destruct Hypothesis less_than_zero (le (S ?) O) 1
-  [<:tactic:<Inversion $0>>].
+  (:tactic:<Inversion $0>).
 
 Then, the tactic is used like this:
 
@@ -91,7 +91,7 @@ hypothesis H.
 
 Similarly for the conclusion :
 
-Hint Destruct Conclusion equal_zero  (? = ?) 1 [<:tactic:<Reflexivity>>].
+Hint Destruct Conclusion equal_zero  (? = ?) 1 (:tactic:<Reflexivity>).
 
 Goal (plus O O)=O.
 DConcl.
@@ -101,7 +101,7 @@ The "Discardable" option clears the hypothesis after using it.
 
 Require DHyp.
 Hint Destruct  Discardable Hypothesis less_than_zero (le (S ?) O) 1
-  [<:tactic:<Inversion $0>>].
+  (:tactic:<Inversion $0>).
 
 Goal (n:nat)(le (S n) O) -> False.
 Intros n H.
@@ -174,8 +174,8 @@ let add (na,dd) =
     | Concl p -> p.d_typ
   in 
   if Nbtermdn.in_dn tactab na then begin
-    mSGNL [< 'sTR "Warning [Overriding Destructor Entry " ; 
-             'sTR (string_of_id na) ; 'sTR"]" >];
+    msgnl (str "Warning [Overriding Destructor Entry " ++ 
+             str (string_of_id na) ++ str"]");
     Nbtermdn.remap tactab na (pat,dd)
   end else 
     Nbtermdn.add tactab (na,(pat,dd))
@@ -192,8 +192,8 @@ let cache_dd (_,(na,dd)) =
     add (na,dd)
   with _ -> 
     anomalylabstrm "Dhyp.add"
-      [< 'sTR"The code which adds destructor hints broke;"; 'sPC; 
-	 'sTR"this is not supposed to happen" >]
+      (str"The code which adds destructor hints broke;" ++ spc () ++ 
+	 str"this is not supposed to happen")
 
 let export_dd x = Some x
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 1e28b23bb3..f7076af256 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -78,7 +78,7 @@ let prolog_tac l n gl =
  (* let l = List.map (pf_interp_constr gl) lcom in *)
   try (prolog l n gl)
   with UserError ("Refiner.tclFIRST",_) ->
-    errorlabstrm "Prolog.prolog" [< 'sTR "Prolog failed" >]
+    errorlabstrm "Prolog.prolog" (str "Prolog failed")
 
 let vernac_prolog =
   let uncom = function
@@ -218,7 +218,7 @@ module SearchProblem = struct
 	  filter_tactics s.tacres
 	    (List.map 
 	       (fun id -> (e_give_exact_constr (mkVar id),
-			   [< 'sTR "Exact"; 'sPC; pr_id id>]))
+			   (str "Exact" ++ spc () ++ pr_id id)))
 	       (pf_ids_of_hyps g))
 	in
 	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
@@ -236,7 +236,7 @@ module SearchProblem = struct
 	     { depth = s.depth; tacres = res; 
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb })
-	  (filter_tactics s.tacres [Tactics.intro,[< 'sTR "Intro" >]])
+	  (filter_tactics s.tacres [Tactics.intro,(str "Intro")])
       in
       let rec_tacs = 
 	let l = 
@@ -259,8 +259,8 @@ module SearchProblem = struct
       List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
 
   let pp s = 
-    mSG (hOV 0 [< 'sTR " depth="; 'iNT s.depth; 'sPC; 
-		  s.last_tactic; 'sTR "\n" >])
+    msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ 
+		  s.last_tactic ++ str "\n"))
 
 end
 
@@ -269,7 +269,7 @@ module Search = Explore.Make(SearchProblem)
 let make_initial_state n gl dblist localdb =
   { SearchProblem.depth = n;
     SearchProblem.tacres = tclIDTAC gl;
-    SearchProblem.last_tactic = [< >];
+    SearchProblem.last_tactic = (mt ());
     SearchProblem.dblist = dblist;
     SearchProblem.localdb = [localdb] }
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index a79186719d..1b56914e92 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -108,7 +108,7 @@ let inductive_of_qualid gls qid =
     | Ind ity -> ity
     | _ ->
 	errorlabstrm "Decompose"
-	  [< Nametab.pr_qualid qid; 'sTR " is not an inductive type" >]
+	  (Nametab.pr_qualid qid ++ str " is not an inductive type")
 
 let decompose_these c l gls =
   let indl = List.map (inductive_of_qualid gls) l in 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ebb6b165f0..aea683dc6e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -217,7 +217,7 @@ let necessary_elimination sort_arity sort =
 	    Type_Type
           else  
 	    errorlabstrm "necessary_elimination" 
-	      [< 'sTR "no primitive equality on proofs" >]  
+	      (str "no primitive equality on proofs")  
     | _ ->
         if is_Set sort_arity then
           Set_SetorProp
@@ -225,7 +225,7 @@ let necessary_elimination sort_arity sort =
           if is_Type sort_arity then
 	    Type_SetorProp
           else  errorlabstrm "necessary_elimination" 
-            [< 'sTR "no primitive equality on proofs" >]
+            (str "no primitive equality on proofs")
 
 let find_eq_pattern aritysort sort = 
   match necessary_elimination aritysort sort with
@@ -429,8 +429,8 @@ let construct_discriminator sigma env dirn c sort =
           CP : changed assert false in a more informative error
        *)
       errorlabstrm "Equality.construct_discriminator"
-	[< 'sTR "Cannot discriminate on inductive constructors with 
-		 dependent types" >] in
+	(str "Cannot discriminate on inductive constructors with 
+		 dependent types") in
   let (mib,mip) = lookup_mind_specif env ind in
   let arsign,arsort = get_arity env indf in
   let (true_0,false_0,sort_0) = 
@@ -473,7 +473,7 @@ let find_eq_data_decompose eqn =
   else if (is_matching (build_coq_idT_pattern ()) eqn) then
     (build_coq_idT_data, match_eq (build_coq_idT_pattern ()) eqn)
   else
-    errorlabstrm  "find_eq_data_decompose" [< >]
+    errorlabstrm  "find_eq_data_decompose" (mt ())
 
 let gen_absurdity id gl =
   if is_empty_type (clause_type (Some id) gl)
@@ -481,7 +481,7 @@ let gen_absurdity id gl =
     simplest_elim (mkVar id) gl
   else
     errorlabstrm "Equality.gen_absurdity" 
-      [< 'sTR "Not the negation of an equality" >]
+      (str "Not the negation of an equality")
 
 (* Precondition: eq is leibniz equality
  
@@ -529,14 +529,14 @@ let discr id gls =
   let (lbeq,(t,t1,t2)) =
     try find_eq_data_decompose eqn
     with e when catchable_exception e ->
-      errorlabstrm "discr"  [<'sTR(string_of_id id); 
-			    'sTR" Not a primitive equality here " >]
+      errorlabstrm "discr"  (str(string_of_id id) ++ 
+			    str" Not a primitive equality here ")
   in
   let sigma = project gls in
   let env = pf_env gls in
   (match find_positions env sigma t1 t2 with
      | Inr _ ->
-	 errorlabstrm "discr" [< 'sTR" Not a discriminable equality" >]
+	 errorlabstrm "discr" (str" Not a discriminable equality")
      | Inl (cpath, (_,dirn), _) ->
 	 let e = pf_get_new_id (id_of_string "ee") gls in
 	 let e_env = push_named_decl (e,None,t) env in
@@ -552,8 +552,8 @@ let discr id gls =
 
 
 let not_found_message id =
-  [<'sTR "The variable"; 'sPC ; 'sTR (string_of_id id) ; 'sPC;
-    'sTR" was not found in the current environment" >]
+  (str "The variable" ++ spc () ++ str (string_of_id id) ++ spc () ++
+    str" was not found in the current environment")
 
 let onNegatedEquality tac gls =
   if is_matching (build_coq_not_pattern ()) (pf_concl gls) then
@@ -562,7 +562,7 @@ let onNegatedEquality tac gls =
     (tclTHEN intro (onLastHyp tac)) gls
   else 
     errorlabstrm "extract_negated_equality_then"
-      [< 'sTR"The goal should negate an equality">]
+      (str"The goal should negate an equality")
 
 let discrClause = function
   | None -> onNegatedEquality discr
@@ -572,7 +572,7 @@ let discrEverywhere =
   tclORELSE
     (Tacticals.tryAllClauses discrClause)
     (fun gls -> 
-       errorlabstrm "DiscrEverywhere" [< 'sTR" No discriminable equalities" >])
+       errorlabstrm "DiscrEverywhere" (str" No discriminable equalities"))
 
 let discrConcl gls  = discrClause None gls
 let discrHyp id gls = discrClause (Some id) gls
@@ -773,19 +773,19 @@ let inj id gls =
     try 
       find_eq_data_decompose eqn
     with e when catchable_exception e -> 
-      errorlabstrm "Inj"  [<'sTR(string_of_id id); 
-			    'sTR" Not a primitive equality here " >] 
+      errorlabstrm "Inj"  (str(string_of_id id) ++ 
+			    str" Not a primitive equality here ") 
   in
   let sigma = project gls in
   let env = pf_env gls in
   match find_positions env sigma t1 t2 with
     | Inl _ ->
 	errorlabstrm "Inj"
-	  [<'sTR (string_of_id id);
-	    'sTR" is not a projectable equality but a discriminable one" >]
+	  (str (string_of_id id) ++
+	    str" is not a projectable equality but a discriminable one")
     | Inr [] ->
 	errorlabstrm "Equality.inj" 
-	   [<'sTR"Nothing to do, it is an equality between convertible terms">]
+	   (str"Nothing to do, it is an equality between convertible terms")
     | Inr posns ->
 	let e = pf_get_new_id (id_of_string "e") gls in
 	let e_env = push_named_decl (e,None,t) env in
@@ -802,7 +802,7 @@ let inj id gls =
 	in
 	if injectors = [] then
 	  errorlabstrm "Equality.inj" 
-	    [<'sTR "Failed to decompose the equality">];
+	    (str "Failed to decompose the equality");
 	tclMAP 
 	  (fun (injfun,resty) ->
 	     let pf = applist(eq.congr (),
@@ -816,7 +816,7 @@ let inj id gls =
                with
 		 | UserError("refiner__fail",_) -> 
 		     errorlabstrm "InjClause" 
-		[< 'sTR (string_of_id id); 'sTR" Not a projectable equality" >]
+		(str (string_of_id id) ++ str" Not a projectable equality")
 	     in ((tclTHENS  (cut  ty) ([tclIDTAC;refine pf]))))
 	  injectors
 	  gls
@@ -853,7 +853,7 @@ let decompEqThen ntac id gls =
 		 refine (mkApp (pf, [| mkVar id |]))]))) gls
      | Inr [] ->
 	 errorlabstrm "Equality.inj" 
-	   [<'sTR"Nothing to do, it is an equality between convertible terms">]
+	   (str"Nothing to do, it is an equality between convertible terms")
      | Inr posns ->
 	 (let e = pf_get_new_id (id_of_string "e") gls in
 	  let e_env = push_named_decl (e,None,t) env in
@@ -870,7 +870,7 @@ let decompEqThen ntac id gls =
 	  in
 	  if injectors = [] then
 	    errorlabstrm "Equality.decompEqThen" 
-              [<'sTR "Discriminate failed to decompose the equality">];
+              (str "Discriminate failed to decompose the equality");
 	  ((tclTHEN
 	      (tclMAP (fun (injfun,resty) ->
 			 let pf = applist(lbeq.congr (),
@@ -901,9 +901,9 @@ let dEqHyp_tac = hide_ident_or_numarg_tactic "DEqHyp" dEqHyp
 
 let rewrite_msg = function 
   | None ->  
-      [<'sTR "passed term is not a primitive equality">] 
+      (str "passed term is not a primitive equality") 
   | Some id ->
-      [<'sTR (string_of_id id); 'sTR "does not satisfy preconditions ">]
+      (str (string_of_id id) ++ str "does not satisfy preconditions ")
 
 let swap_equands gls eqn =
   let (lbeq,(t,e1,e2)) =
@@ -939,12 +939,12 @@ let find_elim  sort_of_gl  lbeq =
 	(match lbeq.rrec with
            | Some eq_rec -> (eq_rec (), false) 
 	   | None -> errorlabstrm "find_elim"
-		 [< 'sTR "this type of elimination is not allowed">])
+		 (str "this type of elimination is not allowed"))
     | _ (* Type *) -> 
         (match lbeq.rect with
            | Some eq_rect -> (eq_rect (), true) 
            | None -> errorlabstrm "find_elim"
-		 [< 'sTR "this type of elimination is not allowed">])
+		 (str "this type of elimination is not allowed"))
 
 (* builds a predicate [e:t][H:(lbeq t e t1)](body e)
    to be used as an argument for equality dependent elimination principle:
@@ -971,7 +971,7 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
       find_elim (pf_type_of gls (pf_concl gls)) lbeq  
     with e when catchable_exception e -> 
       errorlabstrm "RevSubstIncConcl"
-        [< 'sTR "this type of substitution is not allowed">]  
+        (str "this type of substitution is not allowed")  
   in 
   let p =
     if dep then
@@ -1024,7 +1024,7 @@ let find_sigma_data_decompose ex =
        let subst = match_sigma ex (build_coq_existT_pattern ()) in
        (build_sigma_type (),subst)
      with PatternMatchingFailure -> 
-       errorlabstrm "find_sigma_data_decompose" [< >])
+       errorlabstrm "find_sigma_data_decompose" (mt ()))
 
 let decomp_tuple_term env c t = 
   let rec decomprec inner_code ex exty =
@@ -1072,7 +1072,7 @@ let substInConcl eqn gls =
 let substInHyp eqn id gls =
   let (lbeq,(t,e1,e2)) = (find_eq_data_decompose eqn) in 
   let body = subst_term e1 (clause_type (Some id) gls) in
-  if not (dependent (mkRel 1) body) then errorlabstrm  "SubstInHyp" [<>];
+  if not (dependent (mkRel 1) body) then errorlabstrm  "SubstInHyp" (mt ());
   (tclTHENS (cut_replacing id (subst1 e2 body))
      ([tclIDTAC;
        (tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2))
@@ -1088,15 +1088,15 @@ let try_rewrite tac gls =
     tac gls
   with 
     | UserError ("find_eq_data_decompose",_) -> errorlabstrm 
-	  "try_rewrite" [< 'sTR "Not a primitive equality here">]
+	  "try_rewrite" (str "Not a primitive equality here")
     | UserError ("swap_equamds",_) -> errorlabstrm 
-          "try_rewrite" [< 'sTR "Not a primitive equality here">]
+          "try_rewrite" (str "Not a primitive equality here")
     | UserError("find_eq_elim",s) -> errorlabstrm "try_rew" 
-          [<'sTR "This type of elimination is not allowed ">]  
+          (str "This type of elimination is not allowed ")  
     | e when catchable_exception e -> 
 	errorlabstrm "try_rewrite"
-          [< 'sTR "Cannot find a well type generalisation of the goal that";
-             'sTR " makes progress the proof.">]
+          (str "Cannot find a well type generalisation of the goal that" ++
+             str " makes progress the proof.")
 
 (* list_int n 0 [] gives the list [1;2;...;n] *)
 let rec list_int n cmr l =
@@ -1202,7 +1202,7 @@ let general_rewrite_in lft2rgt id (c,lb) gls =
         (match sub_term_with_unif typ_id mbr_eq with
            | None ->
                errorlabstrm "general_rewrite_in" 
-		 [<'sTR "Nothing to rewrite in: "; pr_id id>]
+		 (str "Nothing to rewrite in: " ++ pr_id id)
            | Some (l2,nb_occ) ->
                (tclTHENSI
 		  (tclTHEN
@@ -1248,7 +1248,7 @@ let rewrite_in lR com id gls =
   (try 
      let _ = lookup_named id (pf_env gls) in () 
    with Not_found -> 
-     errorlabstrm "rewrite_in" [< 'sTR"No such hypothesis : " ;pr_id id >]);
+     errorlabstrm "rewrite_in" (str"No such hypothesis : " ++pr_id id));
   let c = pf_interp_constr gls com in
   let eqn = pf_type_of gls c in
   try
@@ -1259,7 +1259,7 @@ let rewrite_in lR com id gls =
           ([tclIDTAC ; exact_no_check c])) gls
      with UserError("SubstInHyp",_) -> tclIDTAC gls)
   with UserError ("find_eq_data_decompose",_)->  
-    errorlabstrm "rewrite_in" [< 'sTR"No equality here" >] 
+    errorlabstrm "rewrite_in" (str"No equality here") 
       
 let subst eqn cls gls =
   match cls with
@@ -1459,7 +1459,7 @@ let sub_list lref i_s i_e =
     else if (i>=i_s) & (i<i_e) then
       sub_list_rec (l@[List.nth lref i]) (i+1)
     else
-      anomalylabstrm "Equality.sub_list" [<'sTR "Out of range">]
+      anomalylabstrm "Equality.sub_list" (str "Out of range")
   in
   sub_list_rec [] i_s
 
@@ -1514,8 +1514,8 @@ type hint_base =
 let explicit_hint_base gl = function 
   | By_name id -> 
       begin match rules_of_base id with
-	| [] -> errorlabstrm "autorewrite" [<'sTR ("Base "^(string_of_id id)^
-						   " does not exist")>]
+	| [] -> errorlabstrm "autorewrite" (str ("Base "^(string_of_id id)^
+						   " does not exist"))
 	| lbs -> lbs
       end 
   | Explicit lbs -> 
@@ -1569,7 +1569,7 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls =
     let cmd = ref cmod
     and wrn = ref warn in
     if !cmd=depth_step then begin
-      wARNING [<'sTR ((string_of_int cglob)^" rewriting(s) carried out") >];
+      msg_warning (str ((string_of_int cglob)^" rewriting(s) carried out"));
       cmd := 0;
       wrn := true
     end;
@@ -1686,7 +1686,7 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls =
     in
     let (gl,lvalid)=
       let (gl_res,lvalid_res,warn)=iterative_rew 0 0 (0,0,false) [g] [] in
-      if warn then mSGNL [<>];
+      if warn then msgnl (mt ());
       (gl_res,lvalid_res)
     in
     let validation_fun=
@@ -1721,7 +1721,7 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls =
   and int_arg=function
     | [(Integer n)] -> n
     | _ -> anomalylabstrm "dyn_autorewrite" 
-	  [<'sTR "Bad call of int_arg (not an INTEGER)">]
+	  (str "Bad call of int_arg (not an INTEGER)")
   and list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest)
     (orest,evorest) (depth,evdepth) = function
       | [] -> (lstep,ostep,lrest,orest,depth)
@@ -1755,13 +1755,13 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls =
 		 (orest,evorest) (dth,true) tail
              else
                errorlabstrm "dyn_autorewrite" 
-		 [<'sTR "Depth value lower or equal to 0">])
+		 (str "Depth value lower or equal to 0"))
 	  else
             anomalylabstrm "dyn_autorewrite" 
-	      [<'sTR "Bad call of list_args_rest">]
+	      (str "Bad call of list_args_rest")
       | _ -> 
 	  anomalylabstrm "dyn_autorewrite" 
-	    [<'sTR "Bad call of list_args_rest">]
+	    (str "Bad call of list_args_rest")
   and list_args = function
     | (Redexp (s,lbases))::tail ->
 	if s = "BaseList" then
@@ -1774,10 +1774,10 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls =
 	     ostep (if lrest=[] then None else Some lrest) orest depth)
 	else
           anomalylabstrm "dyn_autorewrite" 
-	    [<'sTR "Bad call of list_args (not a BaseList tagged REDEXP)">]
+	    (str "Bad call of list_args (not a BaseList tagged REDEXP)")
     | _ ->
 	anomalylabstrm "dyn_autorewrite" 
-	  [<'sTR "Bad call of list_args (not a REDEXP)">]
+	  (str "Bad call of list_args (not a REDEXP)")
   in
   list_args largs*)
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 67e92ac8fe..d639fcf5e7 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -71,7 +71,7 @@ let dest_match_eq gls eqn =
 	  pf_matches gls (Coqlib.build_coq_idT_pattern ()) eqn
         with PatternMatchingFailure ->
 	  errorlabstrm "dest_match_eq" 
-	    [< 'sTR "no primitive equality here" >]))
+	    (str "no primitive equality here")))
     
 (* Environment management *)
 let push_rels vars env =
@@ -95,7 +95,7 @@ let make_inv_predicate env sigma ind id status concl =
       | Dep dflt_concl ->
 	  if not (dependent (mkVar id) concl) then
 	    errorlabstrm "make_inv_predicate"
-              [< 'sTR "Current goal does not depend on "; pr_id id >];
+              (str "Current goal does not depend on " ++ pr_id id);
           (* We abstract the conclusion of goal with respect to
              realargs and c to * be concl in order to rewrite and have
              c also rewritten when the case * will be done *)
@@ -335,10 +335,10 @@ let check_no_metas clenv ccl =
     let metas = List.map (fun n -> Intmap.find n clenv.namenv)
 		  (collect_meta_variables ccl) in
     errorlabstrm "res_case_then" 
-      [< 'sTR ("Cannot find an instantiation for variable"^
-	       (if List.length metas = 1 then " " else "s "));
+      (str ("Cannot find an instantiation for variable"^
+	       (if List.length metas = 1 then " " else "s ")) ++
 	 prlist_with_sep pr_coma pr_id metas
-	 (* ajouter "in "; prterm ccl mais il faut le bon contexte *) >]
+	 (* ajouter "in " ++ prterm ccl mais il faut le bon contexte *))
 
 let res_case_then gene thin indbinding id status gl =
   let env = pf_env gl and sigma = project gl in
@@ -354,7 +354,7 @@ let res_case_then gene thin indbinding id status gl =
     try find_rectype env sigma ccl
     with Induc ->
       errorlabstrm "res_case_then"
-	[< 'sTR ("The type of "^(string_of_id id)^" is not inductive") >] in
+	(str ("The type of "^(string_of_id id)^" is not inductive")) in
   let (elim_predicate,neqns) =
     make_inv_predicate env sigma indt id status (pf_concl gl) in
   let (cut_concl,case_tac) =
@@ -382,22 +382,22 @@ let res_case_then gene thin indbinding id status gl =
 (* Error messages of the inversion tactics *)
 let not_found_message ids =
   if List.length ids = 1 then
-    [<'sTR "the variable"; 'sPC ; 'sTR (string_of_id (List.hd ids)) ; 'sPC;
-      'sTR" was not found in the current environment" >]
+    (str "the variable" ++ spc () ++ str (string_of_id (List.hd ids)) ++ spc () ++
+      str" was not found in the current environment")
   else 
-    [<'sTR "the variables ["; 
-      'sPC ; prlist (fun id -> [<'sTR (string_of_id id) ; 'sPC >]) ids;
-      'sTR" ] were not found in the current environment" >]
+    (str "the variables [" ++ 
+      spc () ++ prlist (fun id -> (str (string_of_id id) ++ spc ())) ids ++
+      str" ] were not found in the current environment")
 
 let dep_prop_prop_message id =
   errorlabstrm "Inv"
-    [< 'sTR "Inversion on "; pr_id id ;
-       'sTR " would needs dependent elimination Prop-Prop" >]
+    (str "Inversion on " ++ pr_id id ++
+       str " would needs dependent elimination Prop-Prop")
  
 let not_inductive_here id =
   errorlabstrm "mind_specif_of_mind"
-    [< 'sTR "Cannot recognize an inductive predicate in "; pr_id id ;
-       'sTR ". If there is one, may be the structure of the arity or of the type of constructors is hidden by constant definitions." >]
+    (str "Cannot recognize an inductive predicate in " ++ pr_id id ++
+       str ". If there is one, may be the structure of the arity or of the type of constructors is hidden by constant definitions.")
 
 (* Noms d'errreurs obsolètes ?? *)
 let wrap_inv_error id = function
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a3bca6d23b..bc3e8ca561 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -37,11 +37,11 @@ open Safe_typing
 let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments"
 
 let no_inductive_inconstr env constr =
-  [< 'sTR "Cannot recognize an inductive predicate in "; 
-     prterm_env env constr;
-     'sTR "."; 'sPC; 'sTR "If there is one, may be the structure of the arity";
-     'sPC; 'sTR "or of the type of constructors"; 'sPC;
-     'sTR "is hidden by constant definitions." >]
+  (str "Cannot recognize an inductive predicate in " ++ 
+     prterm_env env constr ++
+     str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++
+     spc () ++ str "or of the type of constructors" ++ spc () ++
+     str "is hidden by constant definitions.")
 
 (* Inversion stored in lemmas *)
 
@@ -175,9 +175,12 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let revargs,ownsign =
 	fold_named_context
 	  (fun env (id,_,_ as d) (revargs,hyps) ->
-             if List.mem id ivars then ((mkVar id)::revargs,add_named_decl d hyps)
-	     else (revargs,hyps))
-          env ([],[]) in
+             if List.mem id ivars then 
+	       ((mkVar id)::revargs,add_named_decl d hyps)
+	     else 
+	       (revargs,hyps))
+          env ~init:([],[]) 
+      in
       let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
       let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in
       (pty,goal)
@@ -209,7 +212,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
        (ids_of_named_context (named_context invEnv)));
   (*
     errorlabstrm "lemma_inversion"
-    [< 'sTR"Computed inversion goal was not closed in initial signature" >];
+    (str"Computed inversion goal was not closed in initial signature");
   *)
   let invSign = named_context invEnv in
   let pfs = mk_pftreestate (mk_goal invSign invGoal) in
@@ -261,9 +264,9 @@ let inversion_lemma_from_goal n na id sort dep_option inv_op =
   let thin_ids = thin_ids (hyps,fv) in
   if not(list_subset thin_ids fv) then
     errorlabstrm "lemma_inversion"
-      [< 'sTR"Cannot compute lemma inversion when there are" ; 'sPC ;
-	 'sTR"free variables in the types of an inductive" ; 'sPC ;
-	 'sTR"which are not free in its instance" >]; *)
+      (str"Cannot compute lemma inversion when there are" ++ spc () ++
+	 str"free variables in the types of an inductive" ++ spc () ++
+	 str"which are not free in its instance"); *)
   add_inversion_lemma na env sigma t sort dep_option inv_op
    
 open Vernacinterp
@@ -349,8 +352,8 @@ let lemInv id c gls =
  *)
     |  UserError (a,b) -> 
 	 errorlabstrm "LemInv" 
-	   [< 'sTR "Cannot refine current goal with the lemma "; 
-	      prterm_env (Global.env()) c  >] 
+	   (str "Cannot refine current goal with the lemma " ++ 
+	      prterm_env (Global.env()) c) 
 
 let useInversionLemma =
   let gentac =
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 366611d43d..ac1bd4f4f7 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -68,15 +68,15 @@ and  sg_proofs       = (term_with_holes option) list
 (* pour debugger *)
 
 let rec pp_th (TH(c,mm,sg)) =
-  [< 'sTR"TH=[ "; hOV 0 [< prterm c; 'fNL;
-			      (* pp_mm mm; 'fNL; *)
-			   pp_sg sg >] ; 'sTR "]" >]
+  (str"TH=[ " ++ hov 0 (prterm c ++ fnl () ++
+			      (* pp_mm mm ++ fnl () ++ *)
+			   pp_sg sg) ++ str "]")
 and pp_mm l =
-  hOV 0 (prlist_with_sep (fun _ -> [< 'fNL >]) 
-	   (fun (n,c) -> [< 'iNT n; 'sTR" --> "; prterm c >]) l)
+  hov 0 (prlist_with_sep (fun _ -> (fnl ())) 
+	   (fun (n,c) -> (int n ++ str" --> " ++ prterm c)) l)
 and pp_sg sg =
-  hOV 0 (prlist_with_sep (fun _ -> [< 'fNL >])
-	   (function None -> [< 'sTR"None" >] | Some th -> [< pp_th th >]) sg)
+  hov 0 (prlist_with_sep (fun _ -> (fnl ()))
+	   (function None -> (str"None") | Some th -> (pp_th th)) sg)
      
 (*  compute_metamap : constr -> 'a evar_map -> term_with_holes
  *  réalise le 2. ci-dessus
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 0f1b749a62..5c6391dc55 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -156,9 +156,9 @@ let find_theory a =
     setoid_table_find a 
   with Not_found ->
     errorlabstrm "Setoid" 
-      [< 'sTR "No Declared Setoid Theory for ";
-	 prterm a; 'fNL;
-	 'sTR "Use Add Setoid to declare it">]
+      (str "No Declared Setoid Theory for " ++
+	 prterm a ++ fnl () ++
+	 str "Use Add Setoid to declare it")
     
 (* Add a Setoid to the database after a type verification. *)
 
@@ -217,7 +217,7 @@ let gen_eq_lem_name =
 let add_setoid a aeq th =
   if setoid_table_mem a 
   then errorlabstrm "Add Setoid"
-    [< 'sTR "A Setoid Theory is already declared for "; prterm a >]
+    (str "A Setoid Theory is already declared for " ++ prterm a)
   else let env = Global.env () in
     if (is_conv env Evd.empty (Typing.type_of env Evd.empty th)
 	  (mkApp ((Lazy.force coq_Setoid_Theory), [| a; aeq |])))
@@ -230,7 +230,7 @@ let add_setoid a aeq th =
 	  let trans = mkApp ((Lazy.force coq_seq_trans), [|a; aeq; th|]) in
 	  let eq_morph = eq_lem_proof env a aeq sym trans in
 	  let eq_morph2 = eq_lem2_proof env a aeq sym trans in
-	    Options.if_verbose pPNL [< prterm a;'sTR " is registered as a setoid">];
+	    Options.if_verbose ppnl (prterm a ++str " is registered as a setoid");
 	    let eq_ext_name = gen_eq_lem_name () in 
 	    let eq_ext_name2 = gen_eq_lem_name () in 
 	    let _ = Declare.declare_constant eq_ext_name
@@ -251,8 +251,8 @@ let add_setoid a aeq th =
 				     profil = [true; true];
 				     arg_types = [a;a];
 				     lem2 = (Some eqmorph2)})));
-	      Options.if_verbose pPNL [< prterm aeq;'sTR " is registered as a morphism">])
-    else errorlabstrm "Add Setoid" [< 'sTR "Not a valid setoid theory" >]
+	      Options.if_verbose ppnl (prterm aeq ++str " is registered as a morphism"))
+    else errorlabstrm "Add Setoid" (str "Not a valid setoid theory")
 
 (* The vernac command "Add Setoid" *)
 
@@ -302,7 +302,7 @@ let gen_lem_name m = match kind_of_term m with
   | Ind (sp, i) -> add_suffix (basename sp) ((string_of_int i)^"_ext")
   | Construct ((sp,i),j) -> add_suffix
       (basename sp) ((string_of_int i)^(string_of_int i)^"_ext")
-  | _ -> errorlabstrm "New Morphism" [< 'sTR "The term "; prterm m; 'sTR "is not a known name">]
+  | _ -> errorlabstrm "New Morphism" (str "The term " ++ prterm m ++ str "is not a known name")
 
 let gen_lemma_tail m lisset body n =
   let l = (List.length lisset) in
@@ -348,7 +348,7 @@ let gen_compat_lemma env m body larg lisset =
 let new_morphism m id =
   if morphism_table_mem m
   then errorlabstrm "New Morphism"
-    [< 'sTR "The term "; prterm m; 'sTR " is already declared as a morphism">]
+    (str "The term " ++ prterm m ++ str " is already declared as a morphism")
   else 
     let env = Global.env() in
     let typeofm = (Typing.type_of env Evd.empty m) in
@@ -357,10 +357,10 @@ let new_morphism m id =
     let args = (List.rev argsrev) in
       if (args=[])
       then errorlabstrm "New Morphism"
-	[< 'sTR "The term "; prterm m; 'sTR " is not a product">]
+	(str "The term " ++ prterm m ++ str " is not a product")
       else if (check_is_dependent typ (List.length args))
       then  errorlabstrm "New Morphism"
-	[< 'sTR "The term "; prterm m; 'sTR " should not be a dependent product">]
+	(str "The term " ++ prterm m ++ str " should not be a dependent product")
       else (
 	let args_t = (List.map snd args) in
 	let poss = (List.map setoid_table_mem args_t) in
@@ -443,7 +443,7 @@ let gen_lem_iff env m mext larg lisset =
 let add_morphism lem_name (m,profil) =
   if morphism_table_mem m
   then errorlabstrm "New Morphism"
-    [< 'sTR "The term "; prterm m; 'sTR " is already declared as a morpism">]
+    (str "The term " ++ prterm m ++ str " is already declared as a morpism")
   else 
     let env = Global.env() in
     let mext = (current_constant lem_name) in
@@ -478,7 +478,7 @@ let add_morphism lem_name (m,profil) =
 				profil = poss;
 				arg_types = args_t;
 				lem2 = None}))));
-      Options.if_verbose pPNL [< prterm m;'sTR " is registered as a morphism">]   
+      Options.if_verbose ppnl (prterm m ++str " is registered as a morphism")   
     
 let _ = 
   let current_save = vinterp_map "SaveNamed" in
@@ -517,7 +517,7 @@ let _ =
 	      with 
 		  Not_found -> 
 		    errorlabstrm "New Morphism" 
-		      [< 'sTR "The term "; 'sTR(string_of_id s); 'sTR" is not a known name">])
+		      (str "The term " ++ str(string_of_id s) ++ str" is not a known name"))
        | _ -> anomaly "NewMorphism")
 *)
   
@@ -618,7 +618,7 @@ and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
 		  | Some xom -> 
 		      tclTHENS (apply (mkApp (xom, args))) (create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil))
       with Not_found -> errorlabstrm "Setoid_replace" 
-	  [< 'sTR "The term "; prterm c; 'sTR " has not been declared as a morphism">])
+	  (str "The term " ++ prterm c ++ str " has not been declared as a morphism"))
   | ((Prod (_,hh, cc)),(Mimp (hhm, ccm))) ->
       let al = [|hh; cc|] in
       let a = [|hhm; ccm|] in
@@ -644,9 +644,9 @@ and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
   | (_, Toreplace) -> (res_tac gl (pf_type_of glll gl) hyp) (* tclORELSE Auto.full_trivial tclIDTAC *)
   | (_, Tokeep) -> (match hyp with 
 		      | None -> errorlabstrm "Setoid_replace"
-			  [< 'sTR "No replacable occurence of "; prterm c1; 'sTR " found">]
+			  (str "No replacable occurence of " ++ prterm c1 ++ str " found")
 		      | Some _ ->errorlabstrm "Setoid_replace"
-			  [< 'sTR "No rewritable occurence of "; prterm c1; 'sTR " found">])
+			  (str "No rewritable occurence of " ++ prterm c1 ++ str " found"))
   | _ -> anomaly ("Bug in Setoid_replace")) glll
 
 let setoid_replace c1 c2 hyp gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f820fe5fbd..18ec501b86 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -197,13 +197,13 @@ let change_hyp_and_check t env sigma c =
   if is_conv env sigma t c then 
     t
   else 
-    errorlabstrm "convert-check-hyp" [< 'sTR "Not convertible" >]
+    errorlabstrm "convert-check-hyp" (str "Not convertible")
 
 let change_concl_and_check t env sigma c =
   if is_conv_leq env sigma t c then 
     t
   else 
-    errorlabstrm "convert-check-concl" [< 'sTR "Not convertible" >]
+    errorlabstrm "convert-check-concl" (str "Not convertible")
 
 let change_in_concl t = reduct_in_concl (change_concl_and_check t)
 let change_in_hyp t   = reduct_in_hyp (change_hyp_and_check t)
@@ -252,7 +252,7 @@ let dyn_reduce = function
 let unfold_constr = function 
   | ConstRef sp -> unfold_in_concl [[],Closure.EvalConstRef sp]
   | VarRef id -> unfold_in_concl [[],Closure.EvalVarRef id]
-  | _ -> errorlabstrm "unfold_constr" [< 'sTR "Cannot unfold a non-constant.">]
+  | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.")
 
 (*******************************************)
 (*         Introduction tactics            *)
@@ -323,7 +323,7 @@ let rec intro_gen name_flag move_flag force_flag gl =
 	    (intro_gen name_flag move_flag force_flag)) gl)
       with Redelimination ->
         errorlabstrm "Intro" 
-	  [<'sTR "No product even after head-reduction">]
+	  (str "No product even after head-reduction")
     else
       raise e
 
@@ -378,8 +378,8 @@ let rec intros_until s g =
 	  ((tclTHEN (reduce (Red true) []) (intros_until s)) g)
 	with Redelimination ->
           errorlabstrm "Intros" 
-	    [<'sTR ("No hypothesis "^(string_of_id s)^" in current goal");
-	      'sTR " even after head-reduction" >]
+	    (str ("No hypothesis "^(string_of_id s)^" in current goal") ++
+	      str " even after head-reduction")
 
 let rec intros_until_n_gen red n g =
   match pf_lookup_index_as_renamed (pf_concl g) n with
@@ -390,12 +390,12 @@ let rec intros_until_n_gen red n g =
           ((tclTHEN (reduce (Red true) []) (intros_until_n_gen red n)) g)
 	with Redelimination ->
           errorlabstrm "Intros" 
-	    [<'sTR ("No "^(string_of_int n));
-	      'sTR (match n with 1 -> "st" | 2 -> "nd" | _ -> "th");
-	      'sTR " non dependent hypothesis in current goal";
-	      'sTR " even after head-reduction" >]
+	    (str ("No "^(string_of_int n)) ++
+	      str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++
+	      str " non dependent hypothesis in current goal" ++
+	      str " even after head-reduction")
       else
-        errorlabstrm "Intros" [<'sTR "No such hypothesis in current goal" >]
+        errorlabstrm "Intros" (str "No such hypothesis in current goal")
 
 let intros_until_n = intros_until_n_gen true
 let intros_until_n_wored = intros_until_n_gen false
@@ -666,7 +666,7 @@ let generalize_dep c gl =
       d::toquant
     else 
       toquant in
-  let toq_rev = Sign.fold_named_context_reverse seek [] sign in
+  let toq_rev = Sign.fold_named_context_reverse seek ~init:[] sign in
   let qhyps = List.map (fun (id,_,_) -> id) toq_rev in
   let to_quantify =
     List.fold_left
@@ -752,7 +752,7 @@ let letin_abstract id c (occ_ccl,occ_hyps) gl =
       (accu, Some hyp) 
   in
   let (depdecls,marks),_ =
-    fold_named_context_reverse abstract (([],[]),None) env in
+    fold_named_context_reverse abstract ~init:(([],[]),None) env in
   let occ_ccl = if everywhere then Some [] else occ_ccl in
   let ccl = match occ_ccl with
     | None -> pf_concl gl
@@ -1047,7 +1047,7 @@ let elimination_clause_scheme kONT wc elimclause indclause gl =
     (match kind_of_term (last_arg (clenv_template elimclause).rebus) with
        | Meta mv -> mv
        | _  -> errorlabstrm "elimination_clause"
-             [< 'sTR "The type of elimination clause is not well-formed" >]) 
+             (str "The type of elimination clause is not well-formed")) 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause in 
   elim_res_pf kONT elimclause' gl
@@ -1351,7 +1351,7 @@ let cook_sign hyp0 indvars env =
       else
 	Some hyp
   in
-  let _ = fold_named_context seek_deps env None in
+  let _ = fold_named_context seek_deps env ~init:None in
   (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *)
   let compute_lstatus lhyp (hyp,_,_ as d) =
     if hyp = hyp0 then raise (Shunt lhyp);
@@ -1362,7 +1362,7 @@ let cook_sign hyp0 indvars env =
       if List.mem hyp !indhyps then lhyp else (Some hyp) 
   in
   try 
-    let _ = fold_named_context_reverse compute_lstatus None env in
+    let _ = fold_named_context_reverse compute_lstatus ~init:None env in
     anomaly "hyp0 not found"
   with Shunt lhyp0 ->
     let statuslists = (!lstatus,List.rev !rstatus) in
@@ -1447,7 +1447,7 @@ let induction_from_context isrec style hyp0 gl =
   (*test suivant sans doute inutile car refait par le letin_tac*)
   if List.mem hyp0 (ids_of_named_context (Global.named_context())) then
     errorlabstrm "induction" 
-      [< 'sTR "Cannot generalize a global variable" >];
+      (str "Cannot generalize a global variable");
   let tmptyp0 =	pf_get_hyp_typ gl hyp0 in
   let env = pf_env gl in
   let (mind,typ0) = pf_reduce_to_quantified_ind gl tmptyp0 in
@@ -1661,7 +1661,7 @@ let andE id gl =
     (tclTHEN (simplest_elim (mkVar id)) (tclDO 2 intro)) gl
   else 
     errorlabstrm "andE" 
-      [< 'sTR("Tactic andE expects "^(string_of_id id)^" is a conjunction.")>]
+      (str("Tactic andE expects "^(string_of_id id)^" is a conjunction."))
 
 let dAnd cls gl =
   match cls with
@@ -1674,7 +1674,7 @@ let orE id gl =
     (tclTHEN (simplest_elim (mkVar id)) intro) gl
   else 
     errorlabstrm "orE" 
-      [< 'sTR("Tactic orE expects "^(string_of_id id)^" is a disjunction.")>]
+      (str("Tactic orE expects "^(string_of_id id)^" is a disjunction."))
 
 let dorE b cls gl =
   match cls with 
@@ -1689,8 +1689,8 @@ let impE id gl =
        [tclIDTAC;apply_term (mkVar id) [mkMeta (new_meta())]]) gl
   else 
     errorlabstrm "impE"
-      [< 'sTR("Tactic impE expects "^(string_of_id id)^
-	      " is a an implication.")>]
+      (str("Tactic impE expects "^(string_of_id id)^
+	      " is a an implication."))
                         
 let dImp cls gl =
   match cls with
@@ -1748,7 +1748,7 @@ let intros_reflexivity  = (tclTHEN intros reflexivity)
 let dyn_reflexivity = function
   | []  -> intros_reflexivity
   | _ -> errorlabstrm "Tactics.reflexivity" 
-                           [<'sTR "Tactic applied to bad arguments!">]
+                           (str "Tactic applied to bad arguments!")
 
 (* Symmetry tactics *)
 
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 7ccca8c758..f8ad93280e 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -137,7 +137,7 @@ let tauto g =
       (tclORELSE
         (tclTHEN reduction_not_iff (interp (tacticIn tauto_main)))
         (tclTHEN reduction (interp (tacticIn tauto_main))))) g
-  with UserError _ -> errorlabstrm "tauto" [< 'sTR "Tauto failed" >]
+  with UserError _ -> errorlabstrm "tauto" [< str "Tauto failed" >]
 
 let intuition =
   tclTHEN init_intros
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index a8d53dae9c..a233aef2d0 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -63,22 +63,22 @@ let clenv_constrain_with_bindings bl 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");
 		  clenv_lookup_name clause s
               | Nodep n ->
 		  let index = if n > 0 then n-1 else nb_indep+n in
                   if List.mem_assoc (Nodep (index+1)) t or 
                     List.mem_assoc (Nodep (index-nb_indep)) 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 ind_mvs index
 		   with Failure _ ->
                      errorlabstrm "clenv_constrain_with_bindings"
-                       [< 'sTR"Clause did not have " ; 'iNT n ; 'sTR"-th" ;
-                          'sTR" unnamed argument" >])
+                       (str"Clause did not have " ++ int n ++ str"-th" ++
+                          str" unnamed argument"))
               | Abs n -> 
                   (try
                      if n > 0 then 
@@ -88,8 +88,8 @@ let clenv_constrain_with_bindings bl clause =
                      else error "clenv_constrain_with_bindings" 
                    with Failure _ ->
                      errorlabstrm "clenv_constrain_with_bindings"
-                       [< 'sTR"Clause did not have " ; 'iNT n ; 'sTR"-th" ;
-                          'sTR" absolute argument" >])
+                       (str"Clause did not have " ++ int n ++ str"-th" ++
+                          str" absolute argument"))
 	  in
 	  let env = Global.env () in
 	  let sigma = Evd.empty in