X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=aebda4bce746e543ed9d0f102f3329fa22e1bcae;hb=145583de619b9d2fcc4abe3f4d68d01538f9f394;hp=5be36d001756081487505f3d106da63b453d68fe;hpb=1c4968498b6f108cd9c4074c177845a4067cd9d6;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;