diff options
| -rw-r--r-- | stm/stm.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index c966d9bb86..342c16b3b3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1570,11 +1570,15 @@ let collect_proof keep cur hd brkind id = `MaybeASync (parent last, None, accn, name, delegate name) | `Sideff _ -> `Sync (no_name,None,`NestedProof) | _ -> `Sync (no_name,None,`Unknown) in + let make_sync why = function + | `Sync(name,pua,_) -> `Sync (name,pua,why) + | `MaybeASync(_,pua,_,name,_) -> `Sync (name,pua,why) + | `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in + let check_policy rc = if async_policy () then rc else make_sync `Policy rc in match cur, (VCS.visit id).step, brkind with | (parent, { expr = VernacExactProof _ }), `Fork _, _ -> `Sync (no_name,None,`Immediate) - | _ when not (async_policy ()) -> `Sync (no_name,None,`Policy) - | _, _, { VCS.kind = `Edit _ } -> collect (Some cur) [] id + | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) | _ -> if is_defined cur then `Sync (no_name,None,`Transparent) else if keep == VtDrop then `Sync (no_name,None,`Aborted) @@ -1582,12 +1586,8 @@ let collect_proof keep cur hd brkind id = let rc = collect (Some cur) [] id in if keep == VtKeep && (not(State.is_cached id) || !Flags.async_proofs_full) - then rc - else (* we already have the proof, no gain in delaying *) - match rc with - | `Sync(name,pua,_) -> `Sync (name,pua,`AlreadyEvaluated) - | `MaybeASync(_,pua,_,name,_) -> `Sync (name,pua,`AlreadyEvaluated) - | `ASync(_,pua,_,name,_) -> `Sync (name,pua,`AlreadyEvaluated) + then check_policy rc + else make_sync `AlreadyEvaluated rc let string_of_reason = function | `Transparent -> "Transparent" |