From e76659e66a03712e2c9167cef819c2198cf1754d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jan 2019 13:26:46 +0100
Subject: [PATCH] Tactic `iBiOfGoal` that gives the BI of the proof mode goal.

---
 theories/proofmode/ltac_tactics.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 981f0e141..8d313f3bb 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -52,6 +52,9 @@ Ltac iTypeOf H :=
   let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
   pm_eval (envs_lookup H Δ).
 
+Ltac iBiOfGoal :=
+  match goal with |- @envs_entails ?PROP _ _ => PROP end.
+
 Tactic Notation "iMatchHyp" tactic1(tac) :=
   match goal with
   | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
-- 
GitLab