Remove redundancy in section hypotheses of kernel entries.

We only do it for entries and not declarations because the upper layers
rely on the kernel being able to quickly tell that a definition is improperly
used inside a section. Typically, tactics can mess with the named context
and thus make the use of section definitions illegal. This cannot happen in
the kernel but we cannot remove it due to the code dependency.

Probably fixing a soundness bug reachable via ML code only. We were doing
fancy things w.r.t. computation of the transitive closure of the the variables,
in particular lack of proper sanitization of the kernel input.

1 files changed, 1 insertions, 1 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 42d1a1f3fc..c7a588d2b4 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -359,7 +359,7 @@ let save_lemma_admitted ~(lemma : t) : unit =
         let env = Global.env () in
         let ids_typ = Environ.global_vars_set env typ in
         let ids_def = Environ.global_vars_set env pproof in
-        Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
+        Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
       | _ -> None in
   let universes = Proof_global.get_initial_euctx lemma.proof in
   let ctx = UState.check_univ_decl ~poly universes udecl in