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 3270ef451..e8fd76e43 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -326,7 +326,7 @@ let explain_unsolvable_implicit env = function
| BinderType (Name id) ->
str "Cannot infer a type for " ++ Nameops.pr_id id
| BinderType Anonymous ->
- str "Cannot infer a type of this anonymous binder"
+ str "Cannot infer a type for this anonymous binder"
| ImplicitArg (c,n) ->
str "Cannot infer the " ++ pr_ord n ++
str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c