diff options
| author | Pierre-Marie Pédrot | 2016-07-13 17:00:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-07-13 17:00:25 +0200 |
| commit | 9f003b933c2a3504683a84ed817021659e80bc8f (patch) | |
| tree | 4e9636ca44aed009d2274b03e64313c770a8b026 /engine/proofview.ml | |
| parent | 7217d14466bf900ec0353b6bbcb7e4d4b78ec2bf (diff) | |
| parent | 45250332a1e65d434432940a468312f2ab18a2e8 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'engine/proofview.ml')
| -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 905e1c0792..576569cf5f 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 |