From 403a9057b41ed3a8d069175a5834a88442e47f66 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 12 Nov 2020 11:46:24 +0100
Subject: Test case for Proof using in -noinit mode.

---
 test-suite/success/proof_using_noinit.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/success/proof_using_noinit.v

(limited to 'test-suite')

diff --git a/test-suite/success/proof_using_noinit.v b/test-suite/success/proof_using_noinit.v
new file mode 100644
index 0000000000..f99b49619c
--- /dev/null
+++ b/test-suite/success/proof_using_noinit.v
@@ -0,0 +1,9 @@
+(* -*- coq-prog-args: ("-noinit"); -*- *)
+
+Section A.
+Variable A : Prop.
+Hypothesis a : A.
+Lemma b : A.
+Proof using a.
+Admitted.
+End A.
-- 
cgit v1.2.3