Merge branch 'v8.5'

4 files changed, 18 insertions, 17 deletions

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index a76d73006..b8ad996aa 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1265,13 +1265,12 @@ module Make
 
         and pr_tacarg = function
           | TacDynamic (loc,t) ->
-            pr_with_comments loc (
-              str "<" ++ keyword "dynamic" ++ str (" [" ^ (Dyn.tag t)^"]>")
-            )
+            pr_with_comments loc
+              (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>")
           | MetaIdArg (loc,true,s) ->
-            pr_with_comments loc (str ("$" ^ s))
+            pr_with_comments loc (str "$" ++ str s)
           | MetaIdArg (loc,false,s) ->
-            pr_with_comments loc (keyword "constr:" ++ str(" $" ^ s))
+            pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s)
           | Reference r ->
             pr.pr_reference r
           | ConstrMayEval c ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 89ffae4b3..832c08fe0 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -627,6 +627,8 @@ module Make
           )
         | VernacTime v ->
           return (keyword "Time" ++ spc() ++ pr_vernac_list v)
+        | VernacRedirect (s, v) ->
+          return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v)
         | VernacTimeout(n,v) ->
           return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v)
         | VernacFail v ->
@@ -1253,7 +1255,7 @@ module Make
     and pr_extend s cl =
       let pr_arg a =
         try pr_gen a
-        with Failure _ -> str ("<error in "^fst s^">") in
+        with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
       try
         let rl = Egramml.get_extend_vernac_rule s in
         let start,rl,cl =
@@ -1271,7 +1273,7 @@ module Make
             (start,cl) rl in
         hov 1 pp
       with Not_found ->
-        hov 1 (str ("TODO("^fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
+        hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
     in pr_vernac
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 4a66c33df..e50435cda 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -180,16 +180,16 @@ let print_opacity ref =
     | None -> []
     | Some s ->
        [pr_global ref ++ str " is " ++
-        str (match s with
-          | FullyOpaque -> "opaque"
+        match s with
+          | FullyOpaque -> str "opaque"
           | TransparentMaybeOpacified Conv_oracle.Opaque ->
-              "basically transparent but considered opaque for reduction"
+              str "basically transparent but considered opaque for reduction"
           | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev ->
-              "transparent"
+              str "transparent"
           | TransparentMaybeOpacified (Conv_oracle.Level n) ->
-              "transparent (with expansion weight "^string_of_int n^")"
+              str "transparent (with expansion weight " ++ int n ++ str ")"
           | TransparentMaybeOpacified Conv_oracle.Expand ->
-              "transparent (with minimal expansion weight)")]
+              str "transparent (with minimal expansion weight)"]
 
 (*******************)
 (* *)
@@ -386,9 +386,9 @@ let print_located_qualid name flags ref =
     | [] ->
 	let (dir,id) = repr_qualid qid in
 	if DirPath.is_empty dir then
-	  str ("No " ^ name ^ " of basename") ++ spc () ++ pr_id id
+	  str "No " ++ str name ++ str " of basename" ++ spc () ++ pr_id id
 	else
-	  str ("No " ^ name ^ " of suffix") ++ spc () ++ pr_qualid qid
+	  str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid
     | l ->
 	prlist_with_sep fnl
 	(fun (o,oqid) ->
diff --git a/printing/printer.ml b/printing/printer.ml
index 0d3a1c17e..141ae145d 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -654,7 +654,7 @@ let pr_goal_by_id id =
   let p = Proof_global.give_me_the_proof () in
   let g = Goal.get_by_uid id in
   let pr gs =
-    v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut ()
+    v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut ()
 	 ++ pr_goal gs)
   in
   try
@@ -723,7 +723,7 @@ let pr_assumptionset env s =
       try pr_constant env kn
       with Not_found ->
 	let mp,_,lab = repr_con kn in
-	str (string_of_mp mp ^ "." ^ Label.to_string lab)
+        str (string_of_mp mp) ++ str "." ++ pr_label lab
     in
     let safe_pr_ltype typ =
       try str " : " ++ pr_ltype typ