From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 10 Jun 2010 18:23:59 +0000 (+0000)
Subject: Fix for inversion principles of types with a single constructor.
X-Git-Tag: make_still_working~2896
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=145583de619b9d2fcc4abe3f4d68d01538f9f394;p=helm.git

Fix for inversion principles of types with a single constructor.
---

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;