From 7c113b3a736e8a374b8a57aacde846fc5c5cbf3f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 11 May 2020 17:41:58 +0200
Subject: Addressing a suggestion from Théo Zimmermann.

---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3