diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declare.ml | 7 |
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 -> |