From c0e8d5c0ea52cfb0773ce881e6029f1879b1c7cf Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 3 Oct 2019 11:04:51 +0200
Subject: 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.
---
 vernac/lemmas.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

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