diff --git a/src/plugins/wp/TacChoice.ml b/src/plugins/wp/TacChoice.ml
index 3830bf76446d3bb1ef4dfe1ad3c208d963d634ae..76d57c2391060b0bb753e94e62758414c26252db 100644
--- a/src/plugins/wp/TacChoice.ml
+++ b/src/plugins/wp/TacChoice.ml
@@ -64,13 +64,13 @@ class absurd =
       | Clause(Step s) ->
           begin
             match s.condition with
-            | Have p | When p | Core p ->
+            | Have p | When p | Core p | Init p | Type p ->
                 let absurd seq =
                   let emp = Conditions.(step (Have F.p_true)) in
                   let seq = Conditions.replace ~at:s.id emp seq in
                   [ "Absurd" , (fst seq , F.p_not p) ]
                 in Applicable absurd
-            | Init _ | Type _ | Branch _ | Either _ | State _ ->
+            | Branch _ | Either _ | State _ ->
                 Not_applicable
           end
   end
@@ -90,7 +90,7 @@ class contrapose =
       | Clause(Step s) ->
           begin
             match s.condition with
-            | Have p | When p | Core p ->
+            | Have p | When p | Core p | Init p | Type p ->
                 let contrapose (hs,goal) =
                   let descr = "Contrapose" in
                   let goal = F.p_not goal in
@@ -98,7 +98,7 @@ class contrapose =
                   let hs = Conditions.replace ~at:s.id goal (hs , F.p_false) in
                   [ "Contrapose" , (fst hs , F.p_not p) ]
                 in Applicable contrapose
-            | Init _ | Type _ | Branch _ | Either _ | State _ ->
+            | Branch _ | Either _ | State _ ->
                 Not_applicable
           end