Ssreflect's under tactic

[proux01]

The new ssreflect's under tactic https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html?highlight=under#rewriting-under-binders lacks some syntax highlighting and indentation support.

[cpitclaudel]

For these many highlighting issues, I would suggest opening a single meta-issue with a checklist in there. It will reduce noise and make it easier to track progress.