diff options
| author | Enrico Tassi | 2016-09-06 12:57:59 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-09-06 12:57:59 +0200 |
| commit | 5d25643afe3fe0428932e073a23ce3bafb3cb1b1 (patch) | |
| tree | 0c773bbfe82de0178706991913974a332b3ac1b2 | |
| parent | 6745caadf63630c1ad725402fd527ba592dbcd0e (diff) | |
STM: nested Abort is like nested Qed (fix #4756)
There was an "optimization", since Abort is an empty side effect.
But that optimization had an impact on the DAG shape.
Now a nested proof, no matter if it is kept or dropped, is handled the same.
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 9f86597dce..160ca3b6a5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2358,7 +2358,7 @@ let merge_proof_branch ?valid ?id qast keep brname = let id = VCS.new_node ?id () in VCS.merge id ~ours:(Qed (qed None)) brname; VCS.delete_branch brname; - if keep <> VtDrop then VCS.propagate_sideff None; + VCS.propagate_sideff None; `Ok | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } -> let ofp = |