From: Wilmer Ricciotti Date: Wed, 28 Jul 2010 15:45:04 +0000 (+0000) Subject: Fixes unexpected behaviour of ncut when multiple goals are selected. X-Git-Tag: make_still_working~2860 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c76b5031700d8a06d19afb54abc81bf5d34d8242;p=helm.git Fixes unexpected behaviour of ncut when multiple goals are selected. --- 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) =