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/global.ml | |
| 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/global.ml')
| -rw-r--r-- | library/global.ml | 1 |
1 files changed, 0 insertions, 1 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) |