1 2 3 4 5
Open Scope ... (* is not colorized at all, *) Reserved Notation ... (* has only "Notation" colorized, *) Set Implicit Arguments. (* has only "Set" colorized, in a wrong way. *)