From c3e26fca1d077a2b69926df85d05e067882c40b0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 19 Dec 2017 08:33:55 +0100
Subject: Specific type for section definition entries.

This allows to statically ensure well-formedness properties.
---
 kernel/entries.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'kernel/entries.ml')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index ca79de404d..35a1586825 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -81,6 +81,14 @@ type 'a definition_entry = {
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
+type section_def_entry = {
+  secdef_body : constr Univ.in_universe_context_set Future.computation;
+  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 *)
 
 type parameter_entry = 
-- 
cgit v1.2.3


From 1de1d505dfd1c5a05a4910cfc872971087de26fb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 19 Dec 2017 10:11:26 +0100
Subject: 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.
---
 kernel/entries.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel/entries.ml')

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 *)
-- 
cgit v1.2.3