diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 90b495982e..9389a1690b 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -315,8 +315,8 @@ let implicits_of_glob_constr ?(with_products=true) l = if with_products then abs na bk b else (if bk = Implicit then - msg_warning (str "Ignoring implicit status of product binder " ++ - pr_name na ++ str " and following binders"); + msg_warning (strbrk "Ignoring implicit status of product binder " ++ + pr_name na ++ strbrk " and following binders"); []) | GLambda (loc, na, bk, t, b) -> abs na bk b | GLetIn (loc, na, t, b) -> aux i b |