diff options
| author |  Enrico Tassi <enrico.tassi@inria.fr> | 2015-03-25 16:57:31 +0100 |
|---|---|---|
| committer | Enrico Tassi <enrico.tassi@inria.fr> | 2015-03-25 16:57:31 +0100 |
| commit | 99ed6c907c3b2c4901ba51446e0b67696929e02e (patch) | |
| tree | 9eac27605c3ff5c15a97d30d290823e62a9895d1 | |
| parent | 578d73a8b8eb6623bfa688c1e3ed9d1442bd435f (diff) | |
STM: avoid processing asynchronously empty proofs (Close: #4134)
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index d9ecc8bcc..267f08ed5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1638,6 +1638,7 @@ let collect_proof keep cur hd brkind id = | { expr = VernacPrint (PrintName _) } -> true | _ -> false in let parent = function Some (p, _) -> p | None -> assert false in + let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in let rec collect last accn id = let view = VCS.visit id in match view.step with @@ -1687,7 +1688,8 @@ let collect_proof keep cur hd brkind id = else if keep == VtDrop then `Sync (no_name,None,`Aborted) else let rc = collect (Some cur) [] id in - if (keep == VtKeep || keep == VtKeepAsAxiom) && + if is_empty rc then make_sync `AlreadyEvaluated rc + else if (keep == VtKeep || keep == VtKeepAsAxiom) && (not(State.is_cached id) || !Flags.async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc |