From c76b5031700d8a06d19afb54abc81bf5d34d8242 Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 28 Jul 2010 15:45:04 +0000
Subject: [PATCH] Fixes unexpected behaviour of ncut when multiple goals are
 selected.

---
 helm/software/components/ng_tactics/nTactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index f3d74050f..c45e825a4 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -420,12 +420,12 @@ let generalize_tac ~where =
 ;;
 
 let cut_tac t = 
- block_tac [ 
+ atomic_tac (block_tac [ 
   exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
   branch_tac;
    pos_tac [3]; exact_tac t;
    shift_tac; pos_tac [2]; skip_tac;
-  merge_tac ]
+  merge_tac ])
 ;;
 
 let lapply_tac (s,n,t) = 
-- 
2.39.2