From 10e90e268d874b58bf4462677d20dcb893ed0588 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 8 Jun 2020 09:18:34 +0200
Subject: Don't suggest Proof using when no section variables

Fix #12447
---
 vernac/declare.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'vernac')

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 ->
-- 
cgit v1.2.3