From 4f9e0cd748da889622fb7c0cf16a691eb911b9ef Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Feb 2018 01:55:16 +0100
Subject: [PATCH] Support `Absolute` hypotheses in `iModIntro` for `bi_embed`.

---
 theories/proofmode/monpred.v       | 3 +++
 theories/tests/proofmode_monpred.v | 4 ++++
 2 files changed, 7 insertions(+)

diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index df0833cd8..aa15d3dd2 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -354,6 +354,9 @@ Global Instance from_modal_monPred_at i P Q 𝓠 :
   FromModal P Q → MakeMonPredAt i Q 𝓠 → FromModal (P i) 𝓠.
 Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
 *)
+Global Instance into_embed_absolute P :
+  Absolute P → IntoEmbed P (∀ i, P i).
+Proof. rewrite /IntoEmbed=> ?. by rewrite {1}(absolute_absolutely P). Qed.
 End bi.
 
 (* When P and/or Q are evars when doing typeclass search on [IntoWand
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 7475fab4e..70833d974 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -84,6 +84,10 @@ Section tests.
     □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ 𝓟 ∗ 𝓠 ⎤.
   Proof. iIntros "#H1 _ H2 H3". iAlways. iFrame. Qed.
 
+  Lemma test_iModIntro_embed_absolute P `{!Absolute Q} 𝓟 𝓠 :
+    □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ ∀ i, 𝓟 ∗ 𝓠 ∗ Q i ⎤.
+  Proof. iIntros "#H1 H2 H3 H4". iAlways. iFrame. Qed.
+
   (* This is a hack to avoid avoid coq bug #5735: sections variables
      ignore hint modes. So we assume the instances in a way that
      cannot be used by type class resolution, and then declare the
-- 
GitLab