Update test files

5 files changed, 36 insertions, 48 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 ]
diff --git a/etc/coq/multiple/a.v b/etc/coq/multiple/a.v
index 253db19d..d628156e 100644
--- a/etc/coq/multiple/a.v
+++ b/etc/coq/multiple/a.v
@@ -1,11 +1,10 @@
 (* Simple tests for multiple file handling *)
 
-Goal (A,B:Prop)(and A B) -> (and B A).
-Intros A B H.
-Induction H.
-Apply conj.
-Assumption.
-Assumption.
+Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
+  intros A B H.
+  elim H.
+  intros.
+  split.
+  assumption.
+  assumption.
 Save and_comms_a.
-
-
diff --git a/etc/coq/multiple/b.v b/etc/coq/multiple/b.v
index 55c89b76..7e2b7fd3 100644
--- a/etc/coq/multiple/b.v
+++ b/etc/coq/multiple/b.v
@@ -1,11 +1,12 @@
 (* Simple tests for multiple file handling *)
 
-Goal (A,B:Prop)(and A B) -> (and B A).
-Intros A B H.
-Induction H.
-Apply conj.
-Assumption.
-Assumption.
-Save and_comms_b.
-
+Require b1.
 
+Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
+  intros A B H.
+  elim H.
+  intros.
+  split.
+  assumption.
+  assumption.
+Save and_comms_b.
diff --git a/etc/coq/multiple/b2.v b/etc/coq/multiple/b2.v
index b29c5e68..0bccf579 100644
--- a/etc/coq/multiple/b2.v
+++ b/etc/coq/multiple/b2.v
@@ -1 +1,3 @@
+(* b2 -> b1 -> b -> c *)
+
 Parameter b2:Set.
diff --git a/etc/coq/multiple/c.v b/etc/coq/multiple/c.v
index 490c3250..7b15abad 100644
--- a/etc/coq/multiple/c.v
+++ b/etc/coq/multiple/c.v
@@ -1,14 +1,14 @@
 (* Simple tests for multiple file handling *)
 
+Require d.  (* d requires a *)
 Require a.
 Require b.
 
-Goal (A,B:Prop)(and A B) -> (and B A).
-Intros A B H.
-Induction H.
-Apply conj.
-Assumption.
-Assumption.
+Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
+  intros A B H.
+  elim H.
+  intros.
+  split.
+  assumption.
+  assumption.
 Save and_comms_c.
-
-