diff options
| author | Maxime Dénès | 2018-10-01 15:06:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-01 15:06:29 +0200 |
| commit | 2fa8695232363bd23d7963d8af676c4c88b3f07d (patch) | |
| tree | bcd3cc0588e3c3f81c5e923fa52288c5d8ef94b7 /library | |
| parent | c0c3d7f8953323cd5613b0f6c3217f1451a5a060 (diff) | |
| parent | 03bf33b94abcedc8952fd791084c8ffebb695402 (diff) | |
Merge PR #8575: Remove {Safe_typing,Global}.push_context
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 1 | ||||
| -rw-r--r-- | library/global.mli | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/library/global.ml b/library/global.ml index 5872126a12..e872d081d6 100644 --- a/library/global.ml +++ b/library/global.ml @@ -86,7 +86,6 @@ let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) 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) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) diff --git a/library/global.mli b/library/global.mli index 6aeae9fd02..5205968c7b 100644 --- a/library/global.mli +++ b/library/global.mli @@ -49,7 +49,6 @@ val add_mind : (** Extra universe constraints *) val add_constraints : Univ.Constraint.t -> unit -val push_context : bool -> Univ.UContext.t -> unit val push_context_set : bool -> Univ.ContextSet.t -> unit (** Non-interactive modules and module types *) |