Commit f083acae authored by Ralf Jung's avatar Ralf Jung

Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmode

parents e31f8034 4cd7ccda
......@@ -74,4 +74,24 @@ Section tests.
Lemma test_absolutely_affine `{BiAffine PROP} P Q R :
emp - P - Q - R - (P Q).
Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
(* We do not use section variables to avoid coq bug #5735. *)
Instance BU : BUpd PROP. Admitted.
Instance FU : FUpd PROP. Admitted.
Instance FUF : FUpdFacts PROP. Admitted.
Lemma test_apply_fupd_intro_mask E1 E2 P :
E2 E1 P - |={E1,E2}=> |={E2,E1}=> P.
Proof.
iIntros.
(* FIXME : a (PROP:=...) is needed. See #146. *)
Fail iApply fupd_intro_mask.
by iApply (fupd_intro_mask (PROP:=monPredSI)).
Qed.
Lemma test_apply_fupd_intro_mask_2 E1 E2 P :
E2 E1 P - |={E1,E2}=> |={E2,E1}=> P.
Proof.
iIntros. iFrame.
by iApply fupd_intro_mask'. (* But no annotation is needed here *)
Qed.
End tests.
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