X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=aebda4bce746e543ed9d0f102f3329fa22e1bcae;hb=6d49221c1fefe6a2c5bddb3db24d3698414a700f;hp=5be36d001756081487505f3d106da63b453d68fe;hpb=d0e97750e19af9286400a3e7b161a1c658684848;p=helm.git

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 5be36d001..aebda4bce 100644
--- a/helm/software/components/ng_tactics/nInversion.ml
+++ b/helm/software/components/ng_tactics/nInversion.ml
@@ -163,7 +163,7 @@ CicNotationPt.Implicit (`Tagged "end"));
           NTactics.apply_tac ("",0,mk_id "refl"); 
           NTactics.shift_tac;
           elim_tac ~what:("",0,mk_id "Hterm") ~where;
-          NTactics.branch_tac] @ 
+          NTactics.branch_tac ~force:true] @ 
            HExtlib.list_concat ~sep:[NTactics.shift_tac]
             (List.map (fun id-> [NTactics.apply_tac ("",0,mk_id id)]) hyplist) @
          [NTactics.merge_tac;