From 385e6f2309b0bb7e3eac68ec7e8da449e5fc77ef Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Mon, 25 Oct 1999 13:04:22 +0000
Subject: Trivial tests for auto multiple files.

---
 etc/coq/multiple/README |  8 ++++++++
 etc/coq/multiple/a.v    | 11 +++++++++++
 etc/coq/multiple/b.v    | 11 +++++++++++
 etc/coq/multiple/c.v    | 11 +++++++++++
 4 files changed, 41 insertions(+)
 create mode 100644 etc/coq/multiple/README
 create mode 100644 etc/coq/multiple/a.v
 create mode 100644 etc/coq/multiple/b.v
 create mode 100644 etc/coq/multiple/c.v

(limited to 'etc/coq')

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.
+
+
-- 
cgit v1.2.3