Multiple files in PG 3.5 / Coq 8.0

The option "auto-compile-vos" has been fixed up somewhat for this
release.  Please report any problems to David Aspinall (da@inf.ed.ac.uk)

Strategy is:

- When scripting is turned *off* in a buffer, you will be asked if you
want to save it, and then either M-x compile is run (if PG sees a
Makefile in the same directory), or coqc on just the buffer is run.
(You can customize this behaviour by setting compile-command and/or
coq-compile-file-command).
[ Desirable improvement: query user to save any dependent files ]