From 1a4a6f8947afaceb1f7a7f63d31e4d9a7d585db2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 8 Jul 2016 12:05:05 +0200
Subject: Fixing #4906 (regression in printing an error message).

---
 engine/proofview.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 905e1c079..576569cf5 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -366,8 +366,9 @@ let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
     let suffix = !nosuchgoals_hook n in
     CErrors.errorlabstrm ""
-      (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix)
-  | _ -> raise CErrors.Unhandled
+      (str "No such " ++ str (String.plural n "goal") ++ str "." ++
+       pr_non_empty_arg (fun x -> x) suffix)
+      | _ -> raise CErrors.Unhandled
 end
 
 (** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where
-- 
cgit v1.2.3