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, 2 insertions, 6 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 0951b07d49..b88a2e6194 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -161,7 +161,7 @@ type 'opaque result = {
   cook_universes : universes;
   cook_relevance : Sorts.relevance;
   cook_inline : inline;
-  cook_context : Constr.named_context option;
+  cook_context : Id.Set.t option;
 }
 
 let expmod_constr_subst cache modlist subst c =
@@ -242,11 +242,7 @@ let cook_constant { from = cb; info } =
     OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
   | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
   in
-  let const_hyps =
-    Context.Named.fold_outside (fun decl hyps ->
-      List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
-		  hyps)
-      hyps0 ~init:cb.const_hyps in
+  let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in
   let typ = abstract_constant_type (expmod cb.const_type) hyps in
   {
     cook_body = body;