Add simple clear test for multiple files without require

4 files changed, 38 insertions, 0 deletions

diff --git a/etc/coq/multiple-plain/README b/etc/coq/multiple-plain/README
new file mode 100644
index 00000000..6c37325b
--- /dev/null
+++ b/etc/coq/multiple-plain/README
@@ -0,0 +1,8 @@
+Plain tests for multiple file handling, without using require.
+
+Test:
+
+ process a.v
+ process b.v
+ undo a.v, redo a.v
+
diff --git a/etc/coq/multiple-plain/a.v b/etc/coq/multiple-plain/a.v
new file mode 100644
index 00000000..d628156e
--- /dev/null
+++ b/etc/coq/multiple-plain/a.v
@@ -0,0 +1,10 @@
+(* Simple tests for multiple file handling *)
+
+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-plain/b.v b/etc/coq/multiple-plain/b.v
new file mode 100644
index 00000000..aadfeedb
--- /dev/null
+++ b/etc/coq/multiple-plain/b.v
@@ -0,0 +1,10 @@
+(* Simple tests for multiple file handling *)
+
+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-plain/c.v b/etc/coq/multiple-plain/c.v
new file mode 100644
index 00000000..93bf9895
--- /dev/null
+++ b/etc/coq/multiple-plain/c.v
@@ -0,0 +1,10 @@
+(* Simple tests for multiple file handling *)
+
+Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
+  intros A B H.
+  elim H.
+  intros.
+  split.
+  assumption.
+  assumption.
+Save and_comms_c.