diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-15 08:40:13 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-15 08:40:13 +0200 |
| commit | 4703e70b4086bcc14fdd06b3afd98cad0b45157f (patch) | |
| tree | f2a7b925d48ca6ca71d2ae49c310e5c3d934f8fd /stm/stm.ml | |
| parent | 01fa046646398890e64d6effbefd1d2a792dff4e (diff) | |
Fix -async-proofs-always-delegate (close 3740)
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 450259eec..705d427f4 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1228,8 +1228,7 @@ let collect_proof keep cur hd brkind id = else `Sync (name,proof_using_ast last,`Policy) | `Fork((_, hd', GuaranteesOpacity, ids), _) when has_proof_no_using last && not (State.is_cached (parent last)) && - (!Flags.compilation_mode = Flags.BuildVi || - !Flags.async_proofs_always_delegate) -> + !Flags.compilation_mode = Flags.BuildVi -> (try let name = name ids in let hint, time = get_hint_ctx loc, get_hint_bp_time name in |