aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/environ.mli')
-rw-r--r--kernel/environ.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4ad0327fc..9f6ea522a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -208,8 +208,8 @@ val add_constraints : Univ.constraints -> env -> env
(** Check constraints are satifiable in the environment. *)
val check_constraints : Univ.constraints -> env -> bool
-val push_context : Univ.universe_context -> env -> env
-val push_context_set : Univ.universe_context_set -> env -> env
+val push_context : ?strict:bool -> Univ.universe_context -> env -> env
+val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
val push_constraints_to_env : 'a Univ.constrained -> env -> env
val set_engagement : engagement -> env -> env