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.
---
 kernel/safe_typing.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4268f0a602..1069d9a62c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -733,7 +733,7 @@ let constant_entry_of_side_effect eff =
   if Declareops.is_opaque cb then
   OpaqueEff {
     opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
-    opaque_entry_secctx = cb.const_hyps;
+    opaque_entry_secctx = Context.Named.to_vars cb.const_hyps;
     opaque_entry_feedback = None;
     opaque_entry_type = cb.const_type;
     opaque_entry_universes = univs;
@@ -741,7 +741,7 @@ let constant_entry_of_side_effect eff =
   else
   DefinitionEff {
     const_entry_body = p;
-    const_entry_secctx = Some cb.const_hyps;
+    const_entry_secctx = Some (Context.Named.to_vars cb.const_hyps);
     const_entry_feedback = None;
     const_entry_type = Some cb.const_type;
     const_entry_universes = univs;
-- 
cgit v1.2.3