aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-19 10:11:26 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-19 10:52:19 +0100
commit1de1d505dfd1c5a05a4910cfc872971087de26fb (patch)
treee276f4cbf43d9bc2a95ace51b86111852b1f53c4 /library
parentc3e26fca1d077a2b69926df85d05e067882c40b0 (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 'library')
-rw-r--r--library/global.ml2
-rw-r--r--library/global.mli2
2 files changed, 2 insertions, 2 deletions
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)
diff --git a/library/global.mli b/library/global.mli
index 5d7495657..03bc945da 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 ->