Improve comments from #72617, as suggested by RalfJung#73925

Merged

bors merged 2 commits intorust-lang:masterfrom

eduardosm:improve-pr72617-comments

Jul 4, 2020

Commits on Jul 1, 2020

Improve comments from https://github.com/rust-lang/rust/pull/72617, as suggested by RalfJung.
eduardosm
committed

Commits on Jul 2, 2020

Further improve comments in libstd/panicking.rs.
eduardosm
committed