From e1f5de972cbc0eb8d88675366c34ee66aca1b1b4 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Fri, 14 Jan 2011 21:59:26 +0000
Subject: - more coq test cases (some with surprising and embarrassing bugs)

---
 coq/ex/test-cases/require-string/README | 3 +++
 coq/ex/test-cases/require-string/a.v    | 3 +++
 coq/ex/test-cases/require-string/b.v    | 8 ++++++++
 3 files changed, 14 insertions(+)
 create mode 100644 coq/ex/test-cases/require-string/README
 create mode 100644 coq/ex/test-cases/require-string/a.v
 create mode 100644 coq/ex/test-cases/require-string/b.v

(limited to 'coq/ex/test-cases/require-string')

diff --git a/coq/ex/test-cases/require-string/README b/coq/ex/test-cases/require-string/README
new file mode 100644
index 00000000..7b3c5cbe
--- /dev/null
+++ b/coq/ex/test-cases/require-string/README
@@ -0,0 +1,3 @@
+The "Require string" variant is currently not supported.
+
+Here b.v contains Require "a.vo".
diff --git a/coq/ex/test-cases/require-string/a.v b/coq/ex/test-cases/require-string/a.v
new file mode 100644
index 00000000..fc20deef
--- /dev/null
+++ b/coq/ex/test-cases/require-string/a.v
@@ -0,0 +1,3 @@
+(* This file has no dependencies. *)
+
+Definition a := 0.
\ No newline at end of file
diff --git a/coq/ex/test-cases/require-string/b.v b/coq/ex/test-cases/require-string/b.v
new file mode 100644
index 00000000..219c29e2
--- /dev/null
+++ b/coq/ex/test-cases/require-string/b.v
@@ -0,0 +1,8 @@
+(* This file depends on a.v. *)
+
+(* The following works in Proof General 4.0, if a.v has been compiled and
+ * if the path is the correct absolute path.
+ *)
+Require "/home/tews/src/pg/coq/ex/test-cases/require-string/a".
+
+Print a.a.
\ No newline at end of file
-- 
cgit v1.2.3