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

Reviewed-by: ejgallego

3 files changed, 34 insertions, 4 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.
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 7de1ff4083..e3144b2d24 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -911,8 +911,11 @@ end
 
 (* Locality stuff *)
 let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
-  let should_suggest = entry.proof_entry_opaque &&
-                       Option.is_empty entry.proof_entry_secctx in
+  let should_suggest =
+    entry.proof_entry_opaque
+    && not (List.is_empty (Global.named_context()))
+    && Option.is_empty entry.proof_entry_secctx
+  in
   let ubind = UState.universe_binders uctx in
   let dref = match scope with
   | Discharge ->