diff options
| author | Pierre-Marie Pédrot | 2019-10-03 11:04:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-04 17:57:52 +0200 |
| commit | c0e8d5c0ea52cfb0773ce881e6029f1879b1c7cf (patch) | |
| tree | b50900bb768db5c85e34cf338a09cb3a9d928b20 /kernel/cooking.mli | |
| parent | a8ab4cc9bfa9d31ac08b0ae3e3f318578ce50e2a (diff) | |
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.
Diffstat (limited to 'kernel/cooking.mli')
| -rw-r--r-- | kernel/cooking.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 671cdf51fe..83a8b9edfc 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -23,7 +23,7 @@ type 'opaque result = { cook_universes : universes; cook_relevance : Sorts.relevance; cook_inline : inline; - cook_context : Constr.named_context option; + cook_context : Names.Id.Set.t option; } val cook_constant : recipe -> Opaqueproof.opaque result |