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 /kernel/safe_typing.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 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9d302c69fb..b036aa6a67 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -273,7 +273,6 @@ let add_constraints_list cst senv = List.fold_left (fun acc c -> add_constraints c acc) senv cst let push_context_set poly ctx = add_constraints (Now (poly,ctx)) -let push_context poly ctx = add_constraints (Now (poly,Univ.ContextSet.of_context ctx)) let is_curmod_library senv = match senv.modvariant with LIBRARY -> true | _ -> false |