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/entries.ml | |
| 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/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 47e2f72b0e..1e6bc14935 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -61,7 +61,7 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; (* List of section variables *) - const_entry_secctx : Constr.named_context option; + const_entry_secctx : Id.Set.t option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -70,7 +70,7 @@ type definition_entry = { type section_def_entry = { secdef_body : constr; - secdef_secctx : Constr.named_context option; + secdef_secctx : Id.Set.t option; secdef_feedback : Stateid.t option; secdef_type : types option; } @@ -78,7 +78,7 @@ type section_def_entry = { type 'a opaque_entry = { opaque_entry_body : 'a; (* List of section variables *) - opaque_entry_secctx : Constr.named_context; + opaque_entry_secctx : Id.Set.t; (* State id on which the completion of type checking is reported *) opaque_entry_feedback : Stateid.t option; opaque_entry_type : types; @@ -88,7 +88,7 @@ type 'a opaque_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Constr.named_context option * types in_universes_entry * inline + Id.Set.t option * types in_universes_entry * inline type primitive_entry = { prim_entry_type : types option; |