Trivial tests for auto multiple files.

4 files changed, 41 insertions, 0 deletions

diff --git a/etc/coq/multiple/README b/etc/coq/multiple/README
new file mode 100644
index 00000000..6262021a
--- /dev/null
+++ b/etc/coq/multiple/README
@@ -0,0 +1,8 @@
+Quick test for automatic multiple files:
+
+Process a.v, b.v, c.v in turn.
+
+Undo in b.v
+
+Should automatically unlock c.v.
+
diff --git a/etc/coq/multiple/a.v b/etc/coq/multiple/a.v
new file mode 100644
index 00000000..72088498
--- /dev/null
+++ b/etc/coq/multiple/a.v
@@ -0,0 +1,11 @@
+(* Silly tests for automatic auto 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_a.
+
+
diff --git a/etc/coq/multiple/b.v b/etc/coq/multiple/b.v
new file mode 100644
index 00000000..a1a68374
--- /dev/null
+++ b/etc/coq/multiple/b.v
@@ -0,0 +1,11 @@
+(* Silly tests for automatic auto 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.
+
+
diff --git a/etc/coq/multiple/c.v b/etc/coq/multiple/c.v
new file mode 100644
index 00000000..ffdf1d5e
--- /dev/null
+++ b/etc/coq/multiple/c.v
@@ -0,0 +1,11 @@
+(* Silly tests for automatic auto 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_c.
+
+