diff options
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index f8990986c..c9d4afc79 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -339,14 +339,14 @@ let check_correct_manual_implicits autoimps l = List.iter (function | ExplByName id,(b,fi,forced) -> if not forced then - user_err "" + user_err (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".") | ExplByPos (i,_id),_t -> if i<1 || i>List.length autoimps then - user_err "" + user_err (str "Bad implicit argument number: " ++ int i ++ str ".") else - user_err "" + user_err (str "Cannot set implicit argument number " ++ int i ++ str ": it has no name.")) l @@ -665,7 +665,7 @@ let check_inclusion l = let check_rigidity isrigid = if not isrigid then - user_err "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") + user_err (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") let projection_implicits env p impls = let pb = Environ.lookup_projection p env in |