aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index a7c32e1d6..a9f1b7376 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -526,5 +526,5 @@ let _ =
try
coqdep ()
with CErrors.UserError(s,p) ->
- let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in
+ let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in
Feedback.msg_error pp