From 2b92d56815ba5f12394d3f1ab97478bbaa02cf92 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 8 Feb 2019 14:15:41 +0100
Subject: [PATCH] [wp] absurd on type and init
---
src/plugins/wp/TacChoice.ml | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/TacChoice.ml b/src/plugins/wp/TacChoice.ml
index 3830bf76446..76d57c23910 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
--
GitLab