1 files changed, 10 insertions, 24 deletions
diff --git a/etc/coq/multiple/README b/etc/coq/multiple/README
index 48f64110..1450115b 100644
--- a/etc/coq/multiple/README
+++ b/etc/coq/multiple/README
@@ -1,27 +1,13 @@
-New in 3.3: experimental proper handling of multiple files.
-  Not expected to be robust, see comments in coq.el
-  Should be improved for new versions of Coq 7, I hope!
-  Test also for automatic compilation.
+Multiple files in PG 3.5 / Coq 8.0
 
-Expected behaviour: 
+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)
 
-       1) At the end of scripting foo.v (i.e. when activing scripting is
-       switched off), "Reset Initial. Compile Module <foo>" is
-       automatically issued. This clears the context and writes a .vo file,
-       to keep your .vo files up to date. It means that when using PG Coq, 
-       you should use the correct commands ("Require foo.") to load all
-       the modules you depend on, so that scripting can continue in the
-       next file.
+Strategy is:
 
-       2) PG tracks file dependencies by noticing "Reinterning" messages
-       from Coq.  When a file "b.v" is processed which has a "Require a", 
-       command, PG will try to find "a.v" and will automatically lock
-       it.  (This part of the process is fragile, for two reasons: it
-       is hard to find the directory for a.v, since Coq doesn't report
-       it, and the reinterning message is only issued the first time the
-       file is reinterned).
-
-       3) When a file is retracted, PG attempts to automatically unlock
-       all the dependent files, by issuing a coqdep command to determine
-       the dependencies.  (This is a rather nasty hack, it's hoped for
-       the future that Coq will support this functionality directly).
+- 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 ]