Fix broken syntax highlighting for Coq files using "Proof constr".

See Eqdep_dec.v for instance. Module declarations were not highlighted
because the IDE wrongly believed they were used inside an unterminated
proof.
Change an axiom into a definition.
Fix ambiguous regex in syntax highlighting.

This fix considerably speeds up syntax highlighting. It also avoids burning
100% CPU when typing long identifiers. Finally, identifiers longer than 20
characters are now properly highlighted, since the stack of the automaton
no longer overflows because of them.
Properly highlight the Export keyword.
Fix highlighting of "Hint Unfold" and "Hint Rewrite".