aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r--kernel/safe_typing.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d6bd75478..d9adca0c9 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -246,6 +246,8 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e =
else add_constraints (Now (Future.join fc)) e)
{e with future_cst = []} e.future_cst
+let is_joined_environment e = List.is_empty e.future_cst
+
(** {6 Various checks } *)
let exists_modlabel l senv = Label.Set.mem l senv.modlabels