Updated to use Require commands

4 files changed, 10 insertions, 23 deletions

diff --git a/etc/coq/multiple/README b/etc/coq/multiple/README
index b5eab177..03587134 100644
--- a/etc/coq/multiple/README
+++ b/etc/coq/multiple/README
@@ -1,21 +1,5 @@
-Quick test for automatic multiple files:
-
-
-------
-
-1.
-
-Process a.v, b.v, c.v in turn.
-Undo in b.v
-Should automatically unlock c.v.
-
-
-------
-
-2. 
-
-Process as before.  
-Delete buffer b.v.
-Retract in a.v
-
+New in 3.3: experimental proper handling of multiple files.
+  Not expected to be robust, see comments in coq.el
+  Should be improved for Coq 7, I hope!
+  Test also for automatic compilation.
 
diff --git a/etc/coq/multiple/a.v b/etc/coq/multiple/a.v
index 72088498..253db19d 100644
--- a/etc/coq/multiple/a.v
+++ b/etc/coq/multiple/a.v
@@ -1,4 +1,4 @@
-(* Silly tests for automatic auto file handling *)
+(* Simple tests for multiple file handling *)
 
 Goal (A,B:Prop)(and A B) -> (and B A).
 Intros A B H.
diff --git a/etc/coq/multiple/b.v b/etc/coq/multiple/b.v
index a1a68374..55c89b76 100644
--- a/etc/coq/multiple/b.v
+++ b/etc/coq/multiple/b.v
@@ -1,4 +1,4 @@
-(* Silly tests for automatic auto file handling *)
+(* Simple tests for multiple file handling *)
 
 Goal (A,B:Prop)(and A B) -> (and B A).
 Intros A B H.
diff --git a/etc/coq/multiple/c.v b/etc/coq/multiple/c.v
index ffdf1d5e..490c3250 100644
--- a/etc/coq/multiple/c.v
+++ b/etc/coq/multiple/c.v
@@ -1,4 +1,7 @@
-(* Silly tests for automatic auto file handling *)
+(* Simple tests for multiple file handling *)
+
+Require a.
+Require b.
 
 Goal (A,B:Prop)(and A B) -> (and B A).
 Intros A B H.