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.
---
 library/global.ml  | 2 +-
 library/global.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index ce37dfecff..ed847b7cdb 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -81,7 +81,7 @@ let globalize_with_summary fs f =
 let i2l = Label.of_id
 
 let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
-let push_named_def d = globalize (Safe_typing.push_named_def d)
+let push_named_def d = globalize0 (Safe_typing.push_named_def d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 let push_context b c = globalize0 (Safe_typing.push_context b c)
diff --git a/library/global.mli b/library/global.mli
index 5d74956570..03bc945dad 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,7 +32,7 @@ val set_typing_flags : Declarations.typing_flags -> unit
 (** Variables, Local definitions, constants, inductive types *)
 
 val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
-val push_named_def   : (Id.t * Entries.section_def_entry) -> Univ.ContextSet.t
+val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
 
 val export_private_constants : in_section:bool ->
   Safe_typing.private_constants Entries.definition_entry ->
-- 
cgit v1.2.3