diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-08 12:05:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-08 12:05:05 +0200 |
| commit | 1a4a6f8947afaceb1f7a7f63d31e4d9a7d585db2 (patch) | |
| tree | 541a96c06136c2a3d1d71bbd94c7e1123c35dc96 /engine | |
| parent | 8b5cab33d9877f51a5b3e1f2428c08fd07302352 (diff) | |
Fixing #4906 (regression in printing an error message).
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/proofview.ml | 5 |
1 files 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 |