Improvements to the new Coq layer

An official Coq layer was recently added to develop in pull #6911 - thanks to all who made that possible, especially @bixuanzju!

I'm the author of https://github.com/tchajed/spacemacs-coq and use it on a regular basis, and I saw a few changes to the configuration and keybindings in the official layer that I was surprised by. I didn't see any discussion about the customizations in the pull request.

I'd like to have those who use Coq with Spacemacs discuss these changes so we're all happy using the official layer. This is a long list - please feel free to comment on individual points.

1. `company-coq-disabled-features '(hello'): this turns off the company-coq tutorial message; for new users, this should be enabled by default with a prominent note on in the layer README pointing out the tutorial and how to disable the message.
2. In line with other layer READMEs, the layer should point out that it combines proof-general and company-coq.
3. If the settings proof-three-window-mode-policy 'hybrid and proof-script-fly-past-comments t are widely desired, they should be proposed as changes to the proof-general defaults. These options and how to configure them should also be documented in the layer, if people disagree on the right settings.
4. proof-splash-screen t I agree with @cpitclaudel's comment in pull #6911 that this should be enabled, and again the layer can document how to disable it.
5. I personally really like having F2 F3 F4 to navigate proofs, especially because they work equally well as insert mode bindings. The current layer only retains SPC m [, SPC m ] and SPC m .. I'd like to see F2/F3/F4 provided as well (the way my version does), or at least a single layer configuration to enable all of them correctly.
6. It looks like @syl20bnr changed ,pc to ,pi for interrupt and ,px to ,pq for exit. I don't mind the interrupt binding, but I was actually matching the proof-general bindings. I prefer ,pk as a mnemonic for "kill", though.
7. I don't like ,aA/,aB/,aCfor querying at all. I've used my keybindings for some time and they were carefully chosen, but I'd appreciate opinions from others who use Coq significantly if they're experience differs from mine. First, I used n as a mnemonic for "notations", which is really why you would want to show "all". Second, I rarely need to check with implicits or notations, so having memorable shortcuts (like prefixing with "n") works out better for me. I don't mind switching ,ap to ,aa make it faster, though I'm not sure if I print more often then the other queries. It might be worth having a "check if this is a theorem, otherwise print" command from proof-general, which would be a good binding for ,aa.
8. SPC m g l for proof-goto-end-of-locked is a misguided mnemonic; nobody thinks of the currently processed region as "locked", whereas g . to me means "go to the last (processed) period". This is also a case where I mimicked the proof-general keybinding.
9. There's a bug with window-purposes that causes proof-general to kill the current frame when starting the proof process. @aroig provided a fix in #6911 that should be applied. I don't think requiring window-purpose is necessary to give it a post-init, though.
10. smartparens and vi-tilde-fringe are not dependencies of coq; my understanding (based on this description of configuring auto-complete) is that the post-init- functions should not require the layers they configure, and they just won't be called if those packages aren't installed.