From 145583de619b9d2fcc4abe3f4d68d01538f9f394 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 10 Jun 2010 18:23:59 +0000 Subject: [PATCH] Fix for inversion principles of types with a single constructor. --- helm/software/components/ng_tactics/nInversion.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; -- 2.39.2