aboutsummaryrefslogtreecommitdiff
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r--kernel/safe_typing.ml1
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