diff options
| author | Enrico Tassi | 2014-01-04 10:32:22 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-05 17:13:58 +0100 |
| commit | 24ca86389b32e42199db8faadd41918e162b8d46 (patch) | |
| tree | 099e8eae42dfc98eb8ac480f385b2ffec120471b /toplevel | |
| parent | f8970ec2140662274bb10f0eb8d3ca72924835c7 (diff) | |
STM: modules do not prevent proofs from being ASync
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/stm.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index c0ad017583..790a651079 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)) () |