1 files changed, 9 insertions, 9 deletions

diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 0b32cd141..039a42766 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -23,7 +23,7 @@ exception Quit
 
 let disable_drop e =
   if e <> Drop then e
-  else UserError("Vernac.disable_drop",[< 'sTR"Drop is forbidden." >])
+  else UserError("Vernac.disable_drop",(str"Drop is forbidden."))
 
 type vernac_arg = 
   | VARG_VARGLIST of vernac_arg list
@@ -54,7 +54,7 @@ let vinterp_add s f =
     Hashtbl.add vernac_tab s f
   with Failure _ ->
     errorlabstrm "vinterp_add"
-      [< 'sTR"Cannot add the vernac command " ; 'sTR s ; 'sTR" twice" >]
+      (str"Cannot add the vernac command " ++ str s ++ str" twice")
 
 let overwriting_vinterp_add s f =
   begin 
@@ -69,7 +69,7 @@ let vinterp_map s =
     Hashtbl.find vernac_tab s
   with Not_found -> 
     errorlabstrm "Vernac Interpreter"
-      [< 'sTR"Cannot find vernac command " ; 'sTR s >]
+      (str"Cannot find vernac command " ++ str s)
 
 let vinterp_init () = Hashtbl.clear vernac_tab
 
@@ -110,8 +110,8 @@ let rec cvt_varg ast =
       VARG_TACTIC_ARG (interp_tacarg ist targ)
     | Node(_,"VERNACDYN",[Dynamic (_,d)]) -> VARG_DYN d
     | _ -> anomaly_loc (Ast.loc ast, "Vernacinterp.cvt_varg",
-                        [< 'sTR "Unrecognizable ast node of vernac arg:";
-			  'bRK(1,0); print_ast ast >])
+                        (str "Unrecognizable ast node of vernac arg:" ++
+			  brk(1,0) ++ print_ast ast))
 
 (* Interpretation of a vernac command *)
 
@@ -128,7 +128,7 @@ let call (opn,converted_args) =
     | ProtectedLoop -> raise ProtectedLoop
     | e ->
         if !Options.debug then
-	  mSGNL [< 'sTR"Vernac Interpreter " ; 'sTR !loc >];
+	  msgnl (str"Vernac Interpreter " ++ str !loc);
         raise e
 
 let interp = function
@@ -138,14 +138,14 @@ let interp = function
 	  List.map cvt_varg argl
       	with e ->
           if !Options.debug then
-            mSGNL [< 'sTR"Vernac Interpreter " ; 'sTR"Converting arguments" >];
+            msgnl (str"Vernac Interpreter " ++ str"Converting arguments");
           raise e
       in 
       call (opn,converted_args)
   | cmd -> 
       errorlabstrm "Vernac Interpreter"
-        [< 'sTR"Malformed vernac AST : " ; print_ast cmd >]
+        (str"Malformed vernac AST : " ++ print_ast cmd)
 
 let bad_vernac_args s =
   anomalylabstrm s
-    [< 'sTR"Vernac "; 'sTR s; 'sTR" called with bad arguments" >]
+    (str"Vernac " ++ str s ++ str" called with bad arguments")