[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

5 files changed, 17 insertions, 0 deletions

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.