diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-22 15:58:25 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-22 15:58:25 +0100 |
| commit | ff5d440a8158c1ae46604c9557b495e3f45eb077 (patch) | |
| tree | a31d54691159b08077bf2ad652b9de30cf133c51 /library | |
| parent | 3e8ad7726320de5b954675026a4ae429c6c324a8 (diff) | |
| parent | 1de1d505dfd1c5a05a4910cfc872971087de26fb (diff) | |
Merge PR #6469: No universe constraints in Let definitions
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 2 | ||||
| -rw-r--r-- | library/global.mli | 2 |
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 2a646386e..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 * unit Entries.definition_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 -> |