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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/global.ml') diff --git a/library/global.ml b/library/global.ml index ce37dfecf..ed847b7cd 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) -- cgit v1.2.3