diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-19 10:11:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-19 10:52:19 +0100 |
| commit | 1de1d505dfd1c5a05a4910cfc872971087de26fb (patch) | |
| tree | e276f4cbf43d9bc2a95ace51b86111852b1f53c4 /kernel/safe_typing.mli | |
| parent | c3e26fca1d077a2b69926df85d05e067882c40b0 (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 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index faa758d07..757b803a3 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -90,7 +90,7 @@ val push_named_assum : (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : - Id.t * Entries.section_def_entry -> Univ.ContextSet.t safe_transformer + Id.t * Entries.section_def_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) |