From 5d25643afe3fe0428932e073a23ce3bafb3cb1b1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 6 Sep 2016 12:57:59 +0200
Subject: 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.
---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 =
-- 
cgit v1.2.3