Commit 79f576aa authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'robbert/TCEq_hint' into 'master'

Testcase for iris/stdpp!123.

See merge request iris/iris!391
parents 3ffb9bc9 0edc1504
......@@ -11,7 +11,7 @@ synopsis: "This is the Coq development of the Iris Project"
depends: [
"coq" { (>= "8.9.1" & < "8.12~") | (= "dev") }
"coq-stdpp" { (= "dev.2020-03-10.1.20ef8941") | (= "dev") }
"coq-stdpp" { (= "dev.2020-03-10.2.8db97649") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -227,6 +227,9 @@ Proof.
done.
Qed.
Lemma test_iSpecialize_evar P : ( R, R - R) - P - P.
Proof. iIntros "H HP". iApply ("H" with "[HP]"). done. Qed.
Lemma test_iPure_intro_emp R `{!Affine R} :
R - emp.
Proof. iIntros "HR". by iPureIntro. Qed.
......
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