aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/himsg.ml')
-rw-r--r--toplevel/himsg.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 305685cc7..49a1d07f7 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -329,7 +329,7 @@ let explain_occur_check env ev rhs =
str" with term" ++ brk(1,1) ++ pt
let explain_hole_kind env = function
- | QuestionMark -> str "a term for this placeholder"
+ | QuestionMark _ -> str "a term for this placeholder"
| CasesType ->
str "the type of this pattern-matching problem"
| BinderType (Name id) ->