Merge PR #12480: Don't suggest Proof using when no section variables

Reviewed-by: ejgallego

2 files changed, 29 insertions, 2 deletions

diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out
index 8d67a4a4b7..010e217efb 100644
--- a/test-suite/output/SuggestProofUsing.out
+++ b/test-suite/output/SuggestProofUsing.out
@@ -1,7 +1,11 @@
-The proof of nat should start with one of the following commands:
+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. 
+The proof of sec_exactproof should start with one of the following commands:
+Proof using . 
+Proof using Type*. 
+Proof using Type. 
diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v
index 00b6f8e183..69bf8d194a 100644
--- a/test-suite/output/SuggestProofUsing.v
+++ b/test-suite/output/SuggestProofUsing.v
@@ -1,10 +1,22 @@
+Require Program.Tactics.
+
 Set Suggest Proof Using.
 
+Lemma nosec : nat. Proof. exact 0. Qed.
+
+Lemma nosec_exactproof : bool. Proof false.
+
+Program Definition nosec_program : nat := _.
+Next Obligation. exact 1. Qed.
+
+Lemma nosec_abstract : nat.
+Proof. abstract exact 3. Defined.
+
 Section Sec.
   Variables A B : Type.
 
   (* Some normal lemma. *)
-  Lemma nat : Set.
+  Lemma Nat : Set.
   Proof.
     exact nat.
   Qed.
@@ -28,4 +40,15 @@ Section Sec.
     exact A.
   Defined.
 
+  (* No suggest, is this OK? There's nowhere to put it anyway. *)
+  Program Definition program : nat := _.
+  Next Obligation. exact 1. Qed.
+
+  (* Must not suggest *)
+  Lemma sec_abstract : nat.
+  Proof. abstract exact 3. Defined.
+
+  (* Suggests even though there's nowhere to put it, bug? *)
+  Lemma sec_exactproof : bool. Proof true.
+
 End Sec.