]> matita.cs.unibo.it Git - helm.git/commitdiff
Fixes unexpected behaviour of ncut when multiple goals are selected.
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Wed, 28 Jul 2010 15:45:04 +0000 (15:45 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Wed, 28 Jul 2010 15:45:04 +0000 (15:45 +0000)
helm/software/components/ng_tactics/nTactics.ml

index f3d74050f9247cb07cc14d231428c5108ba683da..c45e825a40359ff75fbe464416d19d9bc692760c 100644 (file)
@@ -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) =