Emacs + Proof General + Coq + Windows (for beginners)

I eventually managed to get this working. Here are some quick pointers if you're in a hurry.

1. Use the release version not the beta of Coq (8.4 as of this post). The beta (8.5) caused a couple of errors on my system. First, it spat out Unicode character codes in the middle of command line output - making results unreadable. Second, running Proof General in Emacs then gave an error (something like) 'file specification error replace-regexp-in-string'. I'm not Emacs expert so left it at that.
2. Use the Windows Emacs version from the Emacs site (24.4.1 as of this post).
3. Untar Proof General to a directory of your choice.
4. Add these two lines to your .emacs:
1. (setq coq-prog-name "<PATH-TO-COQ\\bin\\coqtop.exe")
2. (load-file "<PATH-TO-PG>\\generic\\proof-site.el")

Note, if you don't know where to find your '.emacs' configuration file or it doesn't exist, just follow these hints.

Assuming it works, when you create any file in Emacs that ends with the file extension '.v', then you will see a distinct menu-bar with icons appear under the Emacs menus.