STM: cleanup code for Admitted

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"