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 /kernel | |
| parent | c0c3d7f8953323cd5613b0f6c3217f1451a5a060 (diff) | |
| parent | 03bf33b94abcedc8952fd791084c8ffebb695402 (diff) | |
Merge PR #8575: Remove {Safe_typing,Global}.push_context
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 1 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 3 |
2 files changed, 0 insertions, 4 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 diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 08b97b718e..6e0febaa3f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -128,9 +128,6 @@ val add_modtype : val push_context_set : bool -> Univ.ContextSet.t -> safe_transformer0 -val push_context : - bool -> Univ.UContext.t -> safe_transformer0 - val add_constraints : Univ.Constraint.t -> safe_transformer0 |