bors 4760b8fb88 Auto merge of #78179 - RalfJung:miri-comments, r=oli-obk
Miri engine: entirely skip interning of ZST, and improve some comments

r? `@oli-obk`
2020-10-25 20:15:44 +00:00
..