aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/stm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/stm.ml')
-rw-r--r--toplevel/stm.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index c0ad01758..790a65107 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1277,9 +1277,10 @@ let known_state ?(redefine_qed=false) ~cache id =
| `MaybeASync (start, nodes, ids) -> (fun () ->
prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id);
reach ~cache:`Shallow start;
- (* no sections and no modules *)
- if List.is_empty (Environ.named_context (Global.env ())) &&
- Safe_typing.is_curmod_library (Global.safe_env ()) then
+ (* no sections *)
+ if List.is_empty (Environ.named_context (Global.env ()))
+ (* && Safe_typing.is_curmod_library (Global.safe_env ()) *)
+ then
fst (aux (`ASync (start, None, nodes,ids))) ()
else
fst (aux (`Sync `Unknown)) ()