diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 981f0e1419a3c4bcafb3fbe738e993ab6d2d84f8..8d313f3bb6a73f80530f16a5a265297b7fc2992a 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