diff options
| author | Gaëtan Gilbert | 2018-09-27 13:49:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-27 13:49:54 +0200 |
| commit | 03bf33b94abcedc8952fd791084c8ffebb695402 (patch) | |
| tree | d93d8a86007ade9d48678733368ff1cd9ac4707b /library | |
| parent | 49e9fe1c4666beda099872988144d12138dc6349 (diff) | |
Remove {Safe_typing,Global}.push_context
Adding a ucontext to the global environment only makes sense
internally when checking a polymorphic constant.
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 *) |