diff options
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 80bd1ac727..75873381bf 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1810,7 +1810,7 @@ let interp_search_item env sigma = GlobSearchSubPattern (where,head,Pattern.PRef ref) with UserError _ -> user_err ~hdr:"interp_search_item" - (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")) + (str "Unable to interpret " ++ quote (str s) ++ str " as a reference.")) | SearchKind k -> match kind_searcher k with | Inl k -> GlobSearchKind k |