Don't suggest Proof using when no section variables

Fix #12447

1 files changed, 5 insertions, 2 deletions

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 ->