Merge PR #1103: Take Suggest Proof Using outside the kernel.

2 files changed, 38 insertions, 0 deletions

diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out
new file mode 100644
index 0000000000..8d67a4a4b7
--- /dev/null
+++ b/test-suite/output/SuggestProofUsing.out
@@ -0,0 +1,7 @@
+The proof of nat should start with one of the following commands:
+Proof using . 
+Proof using Type*. 
+Proof using Type. 
+The proof of foo should start with one of the following commands:
+Proof using A B. 
+Proof using All. 
diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v
new file mode 100644
index 0000000000..00b6f8e183
--- /dev/null
+++ b/test-suite/output/SuggestProofUsing.v
@@ -0,0 +1,31 @@
+Set Suggest Proof Using.
+
+Section Sec.
+  Variables A B : Type.
+
+  (* Some normal lemma. *)
+  Lemma nat : Set.
+  Proof.
+    exact nat.
+  Qed.
+
+  (* Make sure All is suggested even though we add an unused variable
+  to the context. *)
+  Let foo : Type.
+  Proof.
+    exact (A -> B).
+  Qed.
+
+  (* Having a [Proof using] disables the suggestion message. *)
+  Definition bar : Type.
+  Proof using A.
+    exact A.
+  Qed.
+
+  (* Transparent definitions don't get a suggestion message. *)
+  Definition baz : Type.
+  Proof.
+    exact A.
+  Defined.
+
+End Sec.