diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 751b03a4a..567150a5d 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -310,7 +310,7 @@ let implicits_of_glob_constr ?(with_products=true) l = else let () = match bk with | Implicit -> - msg_warning (strbrk "Ignoring implicit status of product binder " ++ + Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ pr_name na ++ strbrk " and following binders") | _ -> () in [] |