From 3f8273a413183162575f44db946666a26ac0ba8f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 24 Feb 2016 16:42:26 +0100
Subject: [PATCH] Tactic for solving entailment involving just stars.
---
algebra/upred_tactics.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/algebra/upred_tactics.v b/algebra/upred_tactics.v
index 9605b0c36..5e7e2fb2e 100644
--- a/algebra/upred_tactics.v
+++ b/algebra/upred_tactics.v
@@ -117,6 +117,10 @@ Module upred_reflection. Section upred_reflection.
end.
End upred_reflection.
+Tactic Notation "solve_sep_entails" :=
+ upred_reflection.quote; apply upred_reflection.flatten_entails;
+ apply (bool_decide_unpack _); vm_compute; exact Logic.I.
+
Tactic Notation "cancel" constr(Ps) :=
upred_reflection.quote;
match goal with
--
GitLab