Commit 4f9e0cd7 authored by Robbert Krebbers's avatar Robbert Krebbers

Support `Absolute` hypotheses in `iModIntro` for `bi_embed`.

parent 1698a876
......@@ -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
......
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment