Remove emacs header from files?

[jdchristensen]

Our STYLE.md document currently suggests adding an emacs header to all files, but I'd be inclined to remove it, since many people working on the library don't use emacs, and in emacs, you can make this setting yourself (which I do, so the headers aren't useful for me). If we decide to remove these headers, we should also update STYLE.md at the same time.

Based on a comment by @jdchristensen in #2099 (comment)

[SkySkimmer]

It should also be possible to put the setting in dir-locals instead of copying it in every file.

[jdchristensen]

It should also be possible to put the setting in dir-locals instead of copying it in every file.

Oh, right, that's a great idea!

[jdchristensen]

The line we use turns on coq-mode and visual-line-mode. But it doesn't make sense to globally enable coq-mode for every file in the repository, since there are .md files, bash files, python files, etc. Moreover, anyone using proof-general presumably has it set up to open .v files in coq-mode (or maybe that even happens by default if proof-general is installed). So I think I'll just put visual-line-mode in the .dir-locals.el file.