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/term_typing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index c771452a19..4b893b0564 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -18,7 +18,7 @@ type _ trust =
 | Pure : unit trust
 | SideEffects : structure_body -> side_effects trust
 
-val translate_local_def : env -> Id.t -> unit definition_entry ->
+val translate_local_def : env -> Id.t -> section_def_entry ->
   constant_def * types * Univ.ContextSet.t
 
 val translate_local_assum : env -> types -> types
-- 
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/term_typing.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 4b893b0564..7bc029010f 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -19,7 +19,7 @@ type _ trust =
 | SideEffects : structure_body -> side_effects trust
 
 val translate_local_def : env -> Id.t -> section_def_entry ->
-  constant_def * types * Univ.ContextSet.t
+  constr * types
 
 val translate_local_assum : env -> types -> types
 
@@ -72,7 +72,7 @@ val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : trust:'a trust -> env -> Constant.t option -> 
+val infer_declaration : trust:'a trust -> env ->
   'a constant_entry -> Cooking.result
 
 val build_constant_declaration :
-- 
cgit v1.2.3