diff options
| author | Pierre-Marie Pédrot | 2017-12-19 10:11:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-12-19 10:52:19 +0100 |
| commit | 1de1d505dfd1c5a05a4910cfc872971087de26fb (patch) | |
| tree | e276f4cbf43d9bc2a95ace51b86111852b1f53c4 /kernel/entries.ml | |
| parent | c3e26fca1d077a2b69926df85d05e067882c40b0 (diff) | |
Let definitions do not create new universe constraints.
We force the upper layers to extrude the universe constraints before sending
it to the kernel. This simplifies the suspicious handling of polymorphic
constraints for section-local definitions.
Diffstat (limited to 'kernel/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 35a1586825..36b75668b2 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -82,11 +82,10 @@ type 'a definition_entry = { const_entry_inline_code : bool } type section_def_entry = { - secdef_body : constr Univ.in_universe_context_set Future.computation; + secdef_body : constr; secdef_secctx : Context.Named.t option; secdef_feedback : Stateid.t option; secdef_type : types option; - secdef_universes : constant_universes_entry; } type inline = int option (* inlining level, None for no inlining *) |