Added an implicit parameter to branch_tac to allow branching on a

[helm.git] / helm / software / components / ng_tactics / nDestructTac.ml

diff --git a/helm/software/components/ng_tactics/nDestructTac.ml b/helm/software/components/ng_tactics/nDestructTac.ml
index b2faf6d9627df7cb219902797062fc17da946925..103791c03884b79d2cbbff75558efc61ab69e9b5 100644 (file)
--- 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