X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnDestructTac.ml;h=103791c03884b79d2cbbff75558efc61ab69e9b5;hb=d3d800c2489ea484c5e9891f494ca8b07a681c15;hp=b2faf6d9627df7cb219902797062fc17da946925;hpb=d1bda83989a8c07395ec6818a0907f73252bd61e;p=helm.git

diff --git a/helm/software/components/ng_tactics/nDestructTac.ml b/helm/software/components/ng_tactics/nDestructTac.ml
index b2faf6d96..103791c03 100644
--- a/helm/software/components/ng_tactics/nDestructTac.ml
+++ b/helm/software/components/ng_tactics/nDestructTac.ml
@@ -283,7 +283,7 @@ let discriminate_tac ~context cur_eq status =
       leftno m))
       (nbranches-1) [] in
     if nbranches > 1 then
-         NTactics.branch_tac:: branches @ [NTactics.merge_tac]
+         NTactics.branch_tac ~force:false:: branches @ [NTactics.merge_tac]
     else branches
   in