I would want @nikomatsakis  to sign off on these modifications to the documentation before merging