Module vernacular 

Math mode’s colouring, from the kernel’s own vocabulary: its commands (Definition, Inductive, Check, …), the literate forms (## To …:, Consider, When, Yield, ## Theorem: with Statement: and Proof:), the term grammar’s binders and sorts (forall, fun, Prop), and the proof tactics. A test holds these lists to the kernel’s parsers: every keyword they read is coloured, or named here as plain prose.