diff options
| author | Hugo Herbelin | 2020-05-11 17:41:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-15 18:05:11 +0200 |
| commit | 7c113b3a736e8a374b8a57aacde846fc5c5cbf3f (patch) | |
| tree | 53e0163fdb591bbe6db9b253022be99dfe3f0592 | |
| parent | 96333c1bf27f33c15e2475c11c7bfefe87d3a6e1 (diff) | |
Addressing a suggestion from Théo Zimmermann.
| -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 |