Fix for inversion principles of types with a single constructor.

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

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 5be36d001756081487505f3d106da63b453d68fe..aebda4bce746e543ed9d0f102f3329fa22e1bcae 100644 (file)
--- 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;