X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=c45e825a40359ff75fbe464416d19d9bc692760c;hb=d1c9cdb2de96aa2dda6a7b25a4c4959b82b08f6c;hp=f3d74050f9247cb07cc14d231428c5108ba683da;hpb=964844c87f7c3d7061dfeb7f2d84b6b8bbcdaf13;p=helm.git

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) =