Glossary formatting

[RalfJung]

@Lokathor suggested to sort the glossary alphabetically, and I agree that makes sense. We have some PRs in flight that we should land first though, to avoid conflicts.

I am proposing we also change the headers from level 4 to level 3 (#### Term to ### Term). Level 4 has the same font size as normal text, so it looks the same as normal bold text, which can be confusing.

Open Glossary PRs:

• Make niches part of layout and expand call ABI #153
• define (un)sound and UB #190
• Glossary: de-bold paragraph headers #192
• Guarantee the layout of some unions having a single non-zero-sized field #161

[ehsanmok]

I will do that once they are merged.

[RalfJung]

@Lokathor also announced they would do it; please coordinate. :)

[Lokathor]

Oh I've got enough trouble wrangling libm to behave :3 feel free to let anyone else do the glossary thing.

[RalfJung]

All right, @ehsanmok it's yours.

[ehsanmok]

@RalfJung any update on this?

[RalfJung]

Oh, this got lost it seems...

#153 is still open but overall there was not much PR activity recently, so sorting and formatting it now would be fine I think.

[JakobDegen]

Closing as not being tracked in the issues in this repo anymore

[RalfJung]

(I might make a PR to just do these edits)