From 893f8a3a3c573ab6b11cc3938cc67ccdc1b6b4ea Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 24 Feb 2018 16:57:51 +0100
Subject: [test-suite] Add a basic test-case for `Load`.

We test the 3 possible scenarios. A more complete test would also
involved fake_ide.

c.f. #6793
---
 test-suite/output/Load.out              | 6 ++++++
 test-suite/output/Load.v                | 7 +++++++
 test-suite/output/load/Load_noproof.v   | 1 +
 test-suite/output/load/Load_openproof.v | 1 +
 test-suite/output/load/Load_proof.v     | 2 ++
 5 files changed, 17 insertions(+)
 create mode 100644 test-suite/output/Load.out
 create mode 100644 test-suite/output/Load.v
 create mode 100644 test-suite/output/load/Load_noproof.v
 create mode 100644 test-suite/output/load/Load_openproof.v
 create mode 100644 test-suite/output/load/Load_proof.v

(limited to 'test-suite/output')

diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out
new file mode 100644
index 000000000..0904d5540
--- /dev/null
+++ b/test-suite/output/Load.out
@@ -0,0 +1,6 @@
+f = 2
+     : nat
+u = I
+     : True
+The command has indeed failed with message:
+Files processed by Load cannot leave open proofs.
diff --git a/test-suite/output/Load.v b/test-suite/output/Load.v
new file mode 100644
index 000000000..967507415
--- /dev/null
+++ b/test-suite/output/Load.v
@@ -0,0 +1,7 @@
+Load "output/load/Load_noproof.v".
+Print f.
+
+Load "output/load/Load_proof.v".
+Print u.
+
+Fail Load "output/load/Load_openproof.v".
diff --git a/test-suite/output/load/Load_noproof.v b/test-suite/output/load/Load_noproof.v
new file mode 100644
index 000000000..aaf1ffe26
--- /dev/null
+++ b/test-suite/output/load/Load_noproof.v
@@ -0,0 +1 @@
+Definition f := 2.
diff --git a/test-suite/output/load/Load_openproof.v b/test-suite/output/load/Load_openproof.v
new file mode 100644
index 000000000..204d4ecbf
--- /dev/null
+++ b/test-suite/output/load/Load_openproof.v
@@ -0,0 +1 @@
+Lemma k : True.
diff --git a/test-suite/output/load/Load_proof.v b/test-suite/output/load/Load_proof.v
new file mode 100644
index 000000000..e47f66a19
--- /dev/null
+++ b/test-suite/output/load/Load_proof.v
@@ -0,0 +1,2 @@
+Lemma u : True.
+Proof. exact I. Qed.
-- 
cgit v1.2.3